AAAI Publications, Workshops at the Twenty-Seventh AAAI Conference on Artificial Intelligence

Font Size: 
A Formal Framework for the Specification, Verification and Synthesis of Diagnosers
Marco Bozzano, Alessandro Cimatti, Marco Gario, Stefano Tonetta

Last modified: 2013-06-29


In this work we present a formal approach to the design of Fault Detection and Identification (FDI) components. We define 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 procedure 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.


Diagnoser Synthesis; Diagnoser Development; Belief Space; FDI; Model Checking

Full Text: PDF