Formal Verification Workbench for Airbus Avionics Software

International audienceAirbus chose to introduce formal method in his development process for a critical application of the A380 program. This formal verification is used for the Unit Validation and replaces the more traditional method of Unit Testing. By this way, formal method is quietly introduced and doesn't change global process of the development cycle; only design phase and Unit Validation are impacted. A specific method of Unit Proving has been defined in order to use formal verification and proof technology for Unit Validation. The formal verification tool, Caveat, produced by the CEA has been chosen and integrated in a workbench that conforms to the operational, industrial and particular context of use. This experience demonstrates that the use of formal methods for Unit Validation is possible and competitive for a certain category of software