Formal Verification of Critical Aerospace Software

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.