Automated Verification and Tightening of Failure Propagation Models


  • Benjamin Bittner Fondazione Bruno Kessler
  • Marco Bozzano Fondazione Bruno Kessler
  • Alessandro Cimatti Fondazione Bruno Kessler
  • Gianni Zampedri Fondazione Bruno Kessler



timed failure propagation graphs, validation, parameter synthesis, symbolic model checking


Timed Failure Propagation Graphs (TFPGs) are used in the design of safety-critical systems as a way of modeling failure propagation, and to evaluate and implement diagnostic systems. TFPGs are a very rich formalism: they allow to model Boolean combinations of faults and events, also dependent on the operational modes of the system and quantitative delays between them. TFPGs are often produced manually, from a given dynamic system of greater complexity, as abstract representations of the system behavior under specific faulty conditions. In this paper we tackle two key difficulties in this process: first, how to make sure that no important behavior of the system is overlooked in the TFPG, and that no spurious, non-existent behavior is introduced; second, how to devise the correct values for the delays between events. We propose a model checking approach to automatically validate the completeness and tightness of a TFPG for a given infinite-state dynamic system, and a procedure for the automated synthesis of the delay parameters. The proposed approach is evaluated on a number of synthetic and industrial benchmarks.




How to Cite

Bittner, B., Bozzano, M., Cimatti, A., & Zampedri, G. (2016). Automated Verification and Tightening of Failure Propagation Models. Proceedings of the AAAI Conference on Artificial Intelligence, 30(1).



Technical Papers: Knowledge Representation and Reasoning