NASA Logo, National Aeronautics and Space Administration
Intelligent Systems Division Banner

Alexandre Arnold , Airbus

A tour of formal methods in support of aerospace products development

Abstract: From aircrafts to rockets, complex safety-critical systems are at the core of Airbus’ portfolio. For years, formal methods have been key in achieving cutting-edge reliable products. This talk is a wrap-up of success stories and experiments from Airbus at different stages of the development cycle. At System of Systems level, which is of particular interest to Airbus Defence & Space, dealing with scalability is crucial. Statistical Model Checking techniques developed with research partners proved to be up to the task, as demonstrated on various application uses cases related to Air Traffic Management or Emergency Response scenarios. At System level, classical Model Checking has been successfully applied not only on functional models to verify formal requirements, but also on dysfunctional ones to avoid unexpected failure. Examples from the A380 and A350 programs will illustrate both aspects. The industrial use of Hybrid Model Checking and Theorem Proving for verifying more physical systems will also be discussed, with application to satellites. At Software level, static analysis of runtime errors using Abstract Interpretation techniques has been a key enabler of multiple success stories across Airbus divisions. The talk will emphasize the usual process, dealing with false alarms step by step. At Hardware level, formal Worst-Case Execution Time analyses have been explored and improved. A new approach towards multicore schedulability analysis will be presented as an illustration. In spite of all the great applications of formal methods in the aerospace industry, some factors are still limiting their use. Besides, new trends such as autonomous systems create new challenges for tomorrow. This talk will be an opportunity to start the discussion on these aspects and imagine the perspectives for formal methods.

General Chair

Misty Davies
(NASA Ames)

Program Chairs

Clark Barrett
(Stanford University)

Temesghen Kahsai
(NASA Ames / CMU)

Local organization

Guy Katz
(Stanford University)

Rody Kersten
(CMU Silicon Valley)

Program Committee

Aarti Gupta (Princeton)
Alberto Griggio (FBK-IRST)
Alessandro Cimatti (FBK-IRST)
Alwyn Goodloe (NASA Langley)
Arie Gurfinkel (University of Waterloo)
Cesare Tinelli (University of Iowa)
Christoph Torens (German Aerospace Center)
Daniel Kroening (University of Oxford)
Dejan Jovanović (SRI)
Dino Distefano (Facebook)
Dirk Beyer (LMU Munich)
Domagoj Babic (Google)
Ella Atkins (University of Michigan)
Eric Feron (Georgia Tech)
Ewen Denney (SGT / NASA Ames)
Gerwin Klein (NICTA and UNSW)
John Harrison (Intel)
John Rushby (SRI)
Jorge Navas (SRI)
Julia Badger (NASA)
Kalou Cabrera Castillos (LAAS-CNRS)
Kelly Hayhurst (NASA)
Kirstie L. Bellman (The Aerospace Corporation)
Klaus Havelund (NASA JPL)
Kristin Yvonne Rozier (Iowa State University)
Lael Rudd (Draper)
Lee Pike (Galois)
Martin Schäf (SRI)
Mats Heimdahl (University of Minnesota)
Meeko Oishi (University of New Mexico)
Mike Hinchey (Lero-the Irish Software Engineering Research Centre)
Michael Lowry (NASA Ames)
Murali Rangarajan (Boeing)
Natasha Neogi (NASA Langley)
Neha Rungta (AWS)
Nikolaj Bjorner (Microsoft Research)
Patrice Godefroid (Microsoft Research)
Philipp Ruemmer (Uppsala University)
Pierre-Loïc Garoche (ONERA)
Rajeev Joshi (NASA JPL)
Sriram Sankaranarayanan (University of Colorado Boulder)
Susmit Jha (United Technologies)
Virginie Wiels (ONERA)
Wenchao Li (Boston University)
Zvonimir Rakamaric (University of Utah)

First Gov logo
NASA Logo -