Testing and formal verification of behavioral models

Our work seeks better integration of techniques used to verify software development artifacts. An example of application domain is avionics, in collaboration with ONERA and Airbus. Two directions have been explored.

The first one concerns the formal verification of detailed design models used for automated code generation. Currently, the Airbus practice is to test the models in a simulated environment. Our work considers the introduction of model-checking. From our analysis of cases extracted from flight control systems, a key issue concerns the exploitation of counterexamples showing property violation. A counterexample must be interpreted in terms of an operational system-level scenario, and the (unique) counterexample returned by a model-checker is not necessarily realistic from an operational viewpoint [2]. To address this issue, we have proposed an automated structural analysis that identifies parts of the model that are activated by a counterexample over time. This analysis allows us to extract relevant information to explain the observed violation, hence facilitating its interpretation. It also serves to guide the model-checker toward the exploration of different violation patterns (i.e., exhibiting different activation patterns), if needed. 

The second direction concerns the definition of test cases at a higher level of abstraction than what is typically done with current test script languages. The principle is to have declarative and generic descriptions of the test cases, that capture the intent of the tester and can be specialized to different implementation contexts. The descriptions can cover the activation part of test, or the oracle part in charge of establishing a pass/fail verdict. So far, our work has focused on the oracle part. We have defined a solution based on the Lustre language [1]. The specified oracle checks accommodate comparison to expected results with some tolerance in the time and value domains, as well as checks of more general properties relating inputs and outputs. They can be instantiated for several concrete tests. The approach has been successfully applied to industrial examples. Future work on test languages will consider the activation part of the test, and its specialization to various experimental platforms.

Publications

[1] T. Bochot, P. Virelizier, H. Waeselynck, V. Wiels, “Model checking flight control systems: the Airbus experience”, Proc. 31st International Conference on Software Engineering (ICSE 2009), Track Software Engineering in Practice, IEEE CS Press, Vancouver (Canada), May 2009.

[2] G. Durrieu, H. Waeselynck, V. Wiels, “LETO - A lustre-based test oracle for Airbus critical systems”, Proc. 13th Int. ERCIM Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008), L'Aquila (Italy), 15-16 September 2008.