Formal Verification of Critical Aerospace Software


V. Wiels, R. Delmas, D. Doose, P.-L. Garoche, J. Cazin, G. Durrieu

Embedded software is implementing more and more functions in aerospace,
including critical ones. Model Driven Engineering has changed software life cycle development by introducing models in the early steps of software development. Verification and validation is essential, at model and at code levels, and still mostly done by simulation and test. However, formal methods, which are based on the analysis of the program or software model, are being transferred to industry for verification of critical software.
This paper presents the context of aerospace software development, a brief
overview of formal methods and of the associated industrial practice, and the
work done at Onera on formal verification of critical Aerospace software at model and at code levels. This work addresses four themes:

  • Specifics of application of formal methods to aerospace
  • Model driven engineering at platform level
  • Cooperation of analysis techniques
  • Automating test using formal methods

Each of these four themes is a research domain in itself; it is thus impossible
in a single paper to provide a detailed state of the art and an exhaustive list of research challenges for each of them. This paper rather aims at giving a broad vision and at presenting work done at Onera in these domains.

AL04-10.pdf1.31 MB