Dassault Aviation

Formal methods for reliable innovation

Context

Dassault Aviation is a French aerospace company, with over 10,000 aircraft delivered to 90 countries, several offices and plant in the US, and with dual expertise as a manufacturer of both military aircraft (Rafale, nEUROn demonstrator) and business jets (Falcon family). In France and abroad, the company conducts coordinated scientific, technological and industrial actions with partnerships, where innovation is one of the master-keys for success.

Bruno Stoufflet, CTO of Dassault Aviation, says:

“On the one hand, ensuring aircraft safety is obviously mandatory. This is framed by Airworthiness Authorities’ standards. For the related verification activities, static analysis technologies may mathematically help developers consolidate the code behaviors, looking for runtime errors, and in some cases more functional sought properties. On the other hand, with emerging services provided through the Internet and their related threats, from aircraft supply chain to maintenance and industrial systems, cybersecurity must be taken into account in early design steps. Verifying source code by static analysis, in complement to our collaboration with traditional dynamic analyses, is one of the promising means to build even more trustworthy applications. It is expected to increase confidence and resilience, and reduce total development cost by lowering the rework, during further development phases.”

Implementation

“Our teams participated in founding research projects, co-funded initiatives in static analysis, in order to address both safety and security verification goals (beyond quality control objectives), which led to the development of the TrustInSoft tool and service offers.”

Results

“Briefly said, Airworthiness Authorities already acknowledged formal methods in standards. However, obtaining certification credits relies on tool qualification, which requires adapting the process and induces some extra-costs. Regarding cybersecurity, certification bodies’ agreement on formal tool usage for verification is also mandatory. Benefits expected from formal analysis are clearly identified for this purpose. It remains to point out which security evaluation requirements can be duly fulfilled by formal analysis. A consensus must be found by authorities, tool providers, and industrial users on that point.”

“Ensuring aircraft safety is obviously mandatory. This is framed by Airworthiness Authorities’ standards. For the related verification activities, static analysis technologies may mathematically help developers consolidate the code behaviors, looking for runtime errors, and in some cases more functional sought properties.”

Bruno Stoufflet

CTO, Dassault Aviation