Credible autocoding of fault detection observers

Timothy E. Wang, Alireza Esna Ashari, Romain J. Jobredeaux, Eric M. Feron

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Scopus citations

Abstract

We present a domain specific process to enable the verification of observer-based fault detection software. Observer-based fault detection systems, like control systems, yield invariant properties of quadratic types. These quadratic invariants express both safety properties of the software, such as the boundedness of the states, and correctness properties, such as the absence of false alarms from the fault detector. We seek to leverage these quadratic invariants, in an automated way, for the formal verification of the fault detection software. The approach, named the credible autocoding framework, can be characterized as autocoding with proofs. The process starts with the fault detector model, along with its safety and correctness properties, all expressed formally in a synchronous modeling environment such as Simulink. The model is then transformed by a prototype credible autocoder into both code and analyzable annotations for the code. We demonstrate the credible autocoding process on a running example of an output observer fault detector for a 3 degree-of-freedom helicopter control system. © 2014 American Automatic Control Council.
Original languageEnglish (US)
Title of host publicationProceedings of the American Control Conference
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages672-677
Number of pages6
ISBN (Print)9781479932726
DOIs
StatePublished - Jan 1 2014
Externally publishedYes

Fingerprint Dive into the research topics of 'Credible autocoding of fault detection observers'. Together they form a unique fingerprint.

Cite this