Formal Verification of Aerospace Software
Add to Google Calendar
Software plays an ever-increasing role in the design and operation of all aircraft, from UAVs to airliners. On-board software is rigorously developed following the DO-178C norm. Going beyond this rigorous process, this talk shows how to mathematically prove formal guarantees about the correctness of aerospace software, through the example of an industrial aircraft collision avoidance system, ACAS X.
ACAS X is an industrial system intended to be installed on all large aircraft to prevent mid-air collisions. A successor to TCAS, it is being developed by the Federal Aviation Administration. As part of a physical world, ACAS X is a hybrid system: its models are governed by both discrete program constructs as well as differential equations, making verification particularly challenging. I will first determine the geometric configurations under which the advice given by ACAS X is safe, and formally verify these configurations. I will then examine the ACAS X system and analyze some cases where our safe configurations conflict with the advisory given by ACAS X. The approach is general and can be applied to other collision avoidance systems, as well as cars, trains, robots and medical devices.
Jean-Baptiste Jeannin is a starting Assistant Professor in the Department of Aerospace Engineering at the University of Michigan, where his research focuses on formal verification and safety of cyber-physical systems, with a focus on aerospace software systems. His background is in programming languages, logic and security, whose techniques and ideas he applies to the aerospace domain.