The increasing complexity of flight-critical systems (FCS) requires infrastructures that provide high level of confidence and safety assurance. As mandated by DO-178C, its formal method supplement DO-333 and its DO-330 companion document on the development of tools, the ideal tool and method should combine the easiness of use and efficiency of a model based approach with the completeness and verifiability of formal method.
The purpose of this work is to develop multidisciplinary V&V tools and techniques that advance safety assurance and certification of complex flight control systems (FCS). For such purpose, we have designed a toolchain that integrates compilers and formal verification tools to support the development of controllers. Each level of design embed a dedicated formal design language and tools to perform analysis. This framework relies on modular compilation that preserves the hierarchical structure of the controller throughout the compilation. The main emphasis was to ensure functional properties at the appropriate level.
For example, verify global safety properties at the Lustre level, while the analysis of pointers could be done at the C level.
- formal specification
- compilation from model to code
- formal verification
Since the current target is mainly control command software, the synchronous data flow paradigm appears as a de facto standard and the languages Simulink and Lustre are used as model level description languages.