Verification of Cyber-Physical Systems: Temporal Properties and Airplane Collision Avoidance

Add to your list(s) Download to your calendar using vCal

• Jean-Baptiste Jeannin, University of Michigan
• Monday 17 June 2019, 14:00-15:00
• FW26.

If you have a question about this talk, please contact Victor Gomes.

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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.