A formal framework for the specification, verification and synthesis of diagnosers
Marco Bozzano, Alessandro Cimatti, Marco Gario, Stefano Tonetta · 2013
In this work we present a formal approach to the design of Fault Detection and Identification (FDI) components. We de-fine a comprehensive language for the specification of FDI, and discuss how to check whether a given FDI component fulfills its specification. Then, we propose an automatic pro-cedure to synthesize an FDI component that satisfies a given specification. The approach has been implemented and tested in realistic case studies from the aerospace domain.