Verifying robust frequency domain properties of non linear oscillators using SMT

Hafiz Ul Asad; Kevin D. Jones; Frederic Surre

doi:10.1109/DDECS.2014.6868816

Verifying robust frequency domain properties of non linear oscillators using SMT

Hafiz Ul Asad, Kevin D. Jones, Frederic Surre

Faculty of Science and Engineering

City, University of London

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings published in a book › peer-review

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.

Original language	English
Title of host publication	Proceedings of the 2014 IEEE 17th International Symposium on Design and Diagnostics of Electronic Circuits and Systems, DDECS 2014
Editors	Witold Pleskacz, Michel Renovell, Dominik Kasprowicz, Lukas Sekanina, Serge Bernard
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	306-309
Number of pages	4
ISBN (Electronic)	9781479945580
DOIs	https://doi.org/10.1109/DDECS.2014.6868816
Publication status	Published - 30 Jul 2014
Event	17th IEEE International Symposium on Design and Diagnostics of Electronic Circuits and Systems, DDECS 2014 - Warsaw, Poland Duration: 23 Apr 2014 → 25 Apr 2014

Publication series

Name	Proceedings of the 2014 IEEE 17th International Symposium on Design and Diagnostics of Electronic Circuits and Systems, DDECS 2014

Conference

Conference	17th IEEE International Symposium on Design and Diagnostics of Electronic Circuits and Systems, DDECS 2014
Country/Territory	Poland
City	Warsaw
Period	23/04/14 → 25/04/14

ASJC Scopus subject areas

Hardware and Architecture
Control and Systems Engineering
Computer Networks and Communications

Access to Document

10.1109/DDECS.2014.6868816

Cite this

Asad, H. U., Jones, K. D., & 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.), Proceedings of the 2014 IEEE 17th International Symposium on Design and Diagnostics of Electronic Circuits and Systems, DDECS 2014 (pp. 306-309). Article 6868816 (Proceedings of the 2014 IEEE 17th International Symposium on Design and Diagnostics of Electronic Circuits and Systems, DDECS 2014). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/DDECS.2014.6868816

Asad, Hafiz Ul ; Jones, Kevin D. ; Surre, Frederic. / Verifying robust frequency domain properties of non linear oscillators using SMT. Proceedings of the 2014 IEEE 17th International Symposium on Design and Diagnostics of Electronic Circuits and Systems, DDECS 2014. editor / Witold Pleskacz ; Michel Renovell ; Dominik Kasprowicz ; Lukas Sekanina ; Serge Bernard. Institute of Electrical and Electronics Engineers Inc., 2014. pp. 306-309 (Proceedings of the 2014 IEEE 17th International Symposium on Design and Diagnostics of Electronic Circuits and Systems, DDECS 2014).

@inproceedings{87678eb5e0d24b1d818d0ef325837775,

title = "Verifying robust frequency domain properties of non linear oscillators using SMT",

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.",

author = "Asad, {Hafiz Ul} and Jones, {Kevin D.} and Frederic Surre",

note = "Publisher Copyright: {\textcopyright} 2014 IEEE.; 17th IEEE International Symposium on Design and Diagnostics of Electronic Circuits and Systems, DDECS 2014 ; Conference date: 23-04-2014 Through 25-04-2014",

year = "2014",

month = jul,

day = "30",

doi = "10.1109/DDECS.2014.6868816",

language = "English",

series = "Proceedings of the 2014 IEEE 17th International Symposium on Design and Diagnostics of Electronic Circuits and Systems, DDECS 2014",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "306--309",

editor = "Witold Pleskacz and Michel Renovell and Dominik Kasprowicz and Lukas Sekanina and Serge Bernard",

booktitle = "Proceedings of the 2014 IEEE 17th International Symposium on Design and Diagnostics of Electronic Circuits and Systems, DDECS 2014",

address = "United States",

}

Asad, HU, Jones, KD & 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), Proceedings of the 2014 IEEE 17th International Symposium on Design and Diagnostics of Electronic Circuits and Systems, DDECS 2014., 6868816, Proceedings of the 2014 IEEE 17th International Symposium on Design and Diagnostics of Electronic Circuits and Systems, DDECS 2014, Institute of Electrical and Electronics Engineers Inc., pp. 306-309, 17th IEEE International Symposium on Design and Diagnostics of Electronic Circuits and Systems, DDECS 2014, Warsaw, Poland, 23/04/14. https://doi.org/10.1109/DDECS.2014.6868816

Verifying robust frequency domain properties of non linear oscillators using SMT. / Asad, Hafiz Ul; Jones, Kevin D.; Surre, Frederic.
Proceedings of the 2014 IEEE 17th International Symposium on Design and Diagnostics of Electronic Circuits and Systems, DDECS 2014. ed. / Witold Pleskacz; Michel Renovell; Dominik Kasprowicz; Lukas Sekanina; Serge Bernard. Institute of Electrical and Electronics Engineers Inc., 2014. p. 306-309 6868816 (Proceedings of the 2014 IEEE 17th International Symposium on Design and Diagnostics of Electronic Circuits and Systems, DDECS 2014).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings published in a book › peer-review

TY - GEN

T1 - Verifying robust frequency domain properties of non linear oscillators using SMT

AU - Asad, Hafiz Ul

AU - Jones, Kevin D.

AU - Surre, Frederic

PY - 2014/7/30

Y1 - 2014/7/30

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84926663627&partnerID=8YFLogxK

U2 - 10.1109/DDECS.2014.6868816

DO - 10.1109/DDECS.2014.6868816

M3 - Conference proceedings published in a book

AN - SCOPUS:84926663627

T3 - Proceedings of the 2014 IEEE 17th International Symposium on Design and Diagnostics of Electronic Circuits and Systems, DDECS 2014

SP - 306

EP - 309

BT - Proceedings of the 2014 IEEE 17th International Symposium on Design and Diagnostics of Electronic Circuits and Systems, DDECS 2014

A2 - Pleskacz, Witold

A2 - Renovell, Michel

A2 - Kasprowicz, Dominik

A2 - Sekanina, Lukas

A2 - Bernard, Serge

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 17th IEEE International Symposium on Design and Diagnostics of Electronic Circuits and Systems, DDECS 2014

Y2 - 23 April 2014 through 25 April 2014

ER -

Asad HU, Jones KD, Surre F. Verifying robust frequency domain properties of non linear oscillators using SMT. In Pleskacz W, Renovell M, Kasprowicz D, Sekanina L, Bernard S, editors, Proceedings of the 2014 IEEE 17th International Symposium on Design and Diagnostics of Electronic Circuits and Systems, DDECS 2014. Institute of Electrical and Electronics Engineers Inc. 2014. p. 306-309. 6868816. (Proceedings of the 2014 IEEE 17th International Symposium on Design and Diagnostics of Electronic Circuits and Systems, DDECS 2014). doi: 10.1109/DDECS.2014.6868816

Verifying robust frequency domain properties of non linear oscillators using SMT

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this