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.

This paper presents an approach to automate test generation from a formal specification and a set of functional test objectives while taking into account coverage constraints at the specification level. We use existing test generation techniques and tools, our contribution is on the methodological side. We define an innovative approach adapted to the industrial domain and its constraints