Abstract

An increasing number of objects of our physical worlds are controlled by on-board software. This includes cars, trains, airplanes, robots, etc., often grouped under the denomination of cyber-physical systems (CPSs). To ensure that CPSs remain safe to the people and environment surrounding them, it is critical to formally verify their software. But because of their physical nature, CPSs are governed by both discrete program constructs as well as differential equations, making their verification particularly challenging.

In this talk I will first present techniques to express and prove temporal properties about cyber-physical systems. Traditional techniques allow to prove some safety properties about the end state of a system, but temporal properties are more expressive and allow to express and prove properties about the interemediate states reached by the system, thus expressing stronger safety properties as well as liveness properties. I will present a semantics and a proof system for a temporal logic for cyber-physical systems, and show its usefulness on nontrivial properties.

I will then show an application to airplane collision avoidance, with a verification of the next-generation Airborne Collision Avoidance System (ACASX). ACAS X is an industrial system intended to be installed on all large aircraft to give advice to pilots and prevent mid-air collisions with other aircraft. It is currently being developed by the Federal Aviation Administration (FAA). I will determine the geometric configurations under which the advice given by ACAS X is safe and formally verify these configurations. I will then examine the current version of the real ACAS X system and discuss some cases where our safety theorem conflicts with the actual advisory given by that version, demonstrating how formal, hybrid approaches are helping ensure the safety of ACAS X . The approach is general and could also be used to identify unsafe advice issued by other collision avoidance systems or confirm their safety.