City Research Online

Verifying robust frequency domain properties of non linear oscillators using SMT

Ul Asad, H., Jones, K. & Surre, F. (2014). Verifying robust frequency domain properties of non linear oscillators using SMT. In: 17th International Symposium on Design and Diagnostics of Electronic Circuits & Systems. (pp. 306-309). New York, USA: IEEE. ISBN 9781479945580 doi: 10.1109/DDECS.2014.6868816

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: Conference or Workshop Item (Paper)
Subjects: Q Science > QA Mathematics > QA76 Computer software
Departments: School of Science & Technology > Computer Science > Software Reliability
School of Science & Technology > Engineering > Electrical & Electronic Engineering
[img]
Preview
PDF
Download (701kB) | Preview

Export

Downloads

Downloads per month over past year

View more statistics

Actions (login required)

Admin Login Admin Login