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: Pleskacz, W., Renovell, M. & Kasprowicz, D. (Eds.), 17th International Symposium on Design and Diagnostics of Electronic Circuits & Systems. 17th Symposium on Design & Diagnostics of Electronic Circuits & Systems, 23rd - 25th April 2014, Warsaw, Poland. 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 |
Metadata
MetadataActions (login required)
Admin Login