City Research Online

Verifying Robust Frequency Domain Properties of Non Linear Oscillators using SMT

Asad, H., Jones, K. and Surre, F. (2014). Verifying Robust Frequency Domain Properties of Non Linear Oscillators using SMT. In: Pleskacz, W., Renovell, M., Kasprowicz, D., Sekanina, L. and Bernard, S. (Eds.), 17th International Symposium on Design and Diagnostics of Electronic Circuits & Systems. (pp. 306-309). IEEE. ISBN 978-1-4799-4560-3

Abstract

We present a novel mixed time and frequency domain approach to the formal verification of oscillators properties which are specified in the frequency domain. We use robust periodogram specification to specify the oscillator behaviour in the close vicinity of the limit cycle. Using SAT modulo ODE (SMO) for Bounded Model Checking (BMC) of the non-linear hybrid automata, we show that the oscillator hybrid timed traces satisfy frequency domain specifications.

Publication Type: Book Section
Additional Information: © 2014 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Departments: School of Mathematics, Computer Science & Engineering > Computer Science
School of Mathematics, Computer Science & Engineering > Engineering > Electrical & Electronic Engineering
URI: http://openaccess.city.ac.uk/id/eprint/12326
[img]
Preview
Text - Accepted Version
Download (701kB) | Preview

Export

Downloads

Downloads per month over past year

View more statistics

Actions (login required)

Admin Login Admin Login