Formal Specification and Synthesis of FDI through an Example

The correct operation of complex critical systems is increasingly relying on the ability to detect whether (and which) faults are occurring. This task, known as Fault Detection and Identification (FDI), is typically carried out by an FDI component that, observing the sequence of values conveyed by some predefined observables, triggers a set of predefined alarms. An effective FDI system can provide vital information to steer the containment and recovery of faults. We recently proposed a formal framework to support the design of FDI for discrete event systems. The framework is based on a logical language for the specification of FDI requirements and it captures problems such as local diagnosability and maximality, by relying on a semantics based on temporal epistemic logic. This enables the formal verification of the specification and the synthesis of correct-by-construction FDI components. In this paper, we show the merits of the framework by applying it on a simple example, working out the details of the synthesis algorithm, and by reporting the experience on an industrial case-study from the aerospace domain.