Verifying Robust Frequency Domain Properties of Non Linear Oscillators using SMT

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

[img]
Preview
Text - Accepted Version
Download (701kB) | Preview

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.

Item 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
Divisions: School of Informatics
URI: http://openaccess.city.ac.uk/id/eprint/12326

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year

View more statistics