Title: Formal Methods Seminar: Formal Verification of ACAS X, an Industrial Airborne Collision Avoidance System
Speaker: Jean-Baptiste Jeannin, Assistant Professor, University of Michigan – Ann Arbor
Date: Wednesday, November 7, 2018
Location: B1230, R264A
Abstract: 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 an industrial airborne 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 (FAA). 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. 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 show how to verify expressive temporal properties of hybrid systems like ACAS X, including safety and liveness properties. The approach is general and can also be applied to other collision avoidance systems, as well as cars, trains, robots and medical devices.
Bio: Jean-Baptiste Jeannin is an Assistant Professor in the Department of Aerospace Engineering at the University of Michigan – Ann Arbor, 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.