Paths to Property Violation: A Structural Approach for Analyzing Counter-Examples

Abstract

At Airbus, flight control software is developed using SCADE formal models, from which 90% of the code can be generated. Having a formal design leaves open the possibility of introducing model checking techniques. But, from our analysis of cases extracted from real software, a key issue concerns the exploitation of counterexamples showing property violation. Understanding the causes of the violation is not trivial, and the (unique) counterexample returned by a model checker is not necessarily realistic from an operational viewpoint. To address this issue, we propose an automated structural analysis that identifies paths of the model that are activated by a counterexample over time. This analysis allows us to extract relevant information to explain the observed violation. It may also serve to guide the model checker toward the search for different counterexamples, exhibiting new path activation patterns.