@conference {6859131,
	title = {Credible autocoding of fault detection observers},
	booktitle = {American Control Conference (ACC), 2014},
	year = {2014},
	month = {June},
	abstract = {<p>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.</p>},
	keywords = {3-degree-of-freedom helicopter control system, Aerospace Systems, code annotation analysis, control systems, correctness properties, Credible Autocoding, credible autocoding framework, domain specific process, Ellipsoids, Equations, false alarms, Fault detection, fault diagnosis, Formal Methods, formal verification, helicopters, Mathematical model, observer-based fault detection software verification, observers, output observer fault detector model, quadratic-type invariant properties, safety-critical software, Semantics, Simulink, Software, software safety properties, Software Verification, state boundedness, synchronous modeling environment},
	doi = {10.1109/ACC.2014.6859131},
	author = {Timothy Wang and Ashari, A.E. and Romain Jobredeaux and Eric M. Feron}
}