CristalCaveGem Title

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.

These objectives are mainly achieved through three main principles:
  • 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.

A global overview of our approach is provided in IntegratedToolchain.png.
We applied our approach on several use-cases detailed here.

Updated by Arnaud Dieumegard over 8 years ago ยท 11 revisions