City Research Online

Verifying robust frequency domain properties of non linear oscillators using SMT

Ul Asad, Hafiz, Jones, K. and Surre, F. (2014). Verifying robust frequency domain properties of non linear oscillators using SMT. Paper presented at the 17th Symposium on Design & Diagnostics of Electronic Circuits & Systems, 23rd - 25th April 2014, Warsaw, Poland.

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 Mathematics, Computer Science & Engineering > Computer Science > Software Reliability
School of Mathematics, Computer Science & Engineering > Engineering > Electrical & Electronic Engineering
URI: http://openaccess.city.ac.uk/id/eprint/3405
[img]
Preview
PDF
Download (701kB) | Preview

Export

Downloads

Downloads per month over past year

View more statistics

Actions (login required)

Admin Login Admin Login