Login | Register

Formal verification of bond graph modelled analogue circuits


Formal verification of bond graph modelled analogue circuits

Denman, W., Zaki, M.H. and Tahar, Sofiène (2011) Formal verification of bond graph modelled analogue circuits. IET Circuits, Devices & Systems, 5 (3). p. 243. ISSN 1751858X

[thumbnail of IET-2011.pdf]
Text (application/pdf)
IET-2011.pdf - Accepted Version

Official URL: http://dx.doi.org/10.1049/iet-cds.2009.0221


Analogue circuits are an increasingly critical component in embedded system designs. Traditionally, simulation is used for verification, but owing to the infinite state space of analogue components, the 100% correctness of a design cannot be guaranteed. Formal methods, based around applying mathematical expressions and reasoning to prove correctness, have been developed to increase the verification confidence level. This study introduces and demonstrates a methodology for formally verifying safety properties of analogue circuits. In the proposed approach, system equations are automatically extracted from a SPICE netlist by means of energy-conservative bond graph models. Verification based on abstract model checking and constraint solving is then applied on the extracted equation models. The authors methodology avoids an exhaustive and time demanding simulation that is normally encountered during analogue circuit verification. To this end, the authors have used a set of tools to implement the proposed verification flow and applied it on tunnel diode, Chua and Colpitts oscillators as case studies.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Article
Authors:Denman, W. and Zaki, M.H. and Tahar, Sofiène
Journal or Publication:IET Circuits, Devices & Systems
Digital Object Identifier (DOI):10.1049/iet-cds.2009.0221
Keywords:formal verification; analogue circuits; tunnel diode oscillators; Chua's circuit; bond graphs; mathematical analysis
ID Code:977363
Deposited By: Danielle Dennie
Deposited On:14 Jun 2013 14:00
Last Modified:18 Jan 2018 17:44
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top