Using Formal Methods and Testability Concepts in the Avionics Systems Validation and Verification (V&V) Process

Airbus has used formal methods for several years to specify avionics systems. Thanks to these methods, formal verification, testability concepts and automatic test case generation were explored and experimented on Airbus systems. This paper depicts the Airbus validation and verification process all along the system development cycle pointing out what kinds of static analysis and dynamic verification and validation activities are conducted. Then, we focus on innovative methods based on testing strategies for traceability purposes, testing design and fault isolation. Some considerations related to automatic test case generation are also discussed.