Portal de Periódicos da CAPES

Automated Verification and Tightening of Failure Propagation Models

2016; Association for the Advancement of Artificial Intelligence; Volume: 30; Issue: 1 Linguagem: Inglês

10.1609/aaai.v30i1.10094

2374-3468

Benjamin Bittner, Marco Bozzano, Alessandro Cimatti, Gianni Zampedri,

Software Reliability and Analysis Research

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.