2013/11/08 by Timothy C. Wang, Alireza Esna Ashari, Wang, Timothy +5
Computer Science · Engineering · #FOS: Electrical engineering #Fault Detection and Control Systems #Formal Methods in Verification #Software Reliability and Analysis Research #Systems and Control (eess.SY) #electronic engineering #information engineering
paper · pdf · doi:10.48550/arxiv.1311.2064
openalex publication_date 2013/11/08 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
In this paper, we present a domain specific process to assist 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 fashion, for the formal verification of the fault detection software. The approach, referred to as the credible autocoding framework [1], 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-degrees-of-freedom (3DOF) helicopter control system.