BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verification of Cyber-Physical Systems: Temporal Properties and Ai
 rplane Collision Avoidance - Jean-Baptiste Jeannin\,  University of Michig
 an
DTSTART:20190617T130000Z
DTEND:20190617T140000Z
UID:TALK125878@talks.cam.ac.uk
CONTACT:Victor Gomes
DESCRIPTION:An increasing number of objects of our physical worlds are con
 trolled by on-board software. This includes cars\, trains\, airplanes\, ro
 bots\, etc.\, often grouped under the denomination of cyber-physical syste
 ms (CPSs). To ensure that CPSs remain safe to the people and environment s
 urrounding them\, it is critical to formally verify their software. But be
 cause of their physical nature\, CPSs are governed by both discrete progra
 m constructs as well as differential equations\, making their verification
  particularly challenging.\n\nIn this talk I will first present techniques
  to express and prove temporal properties about cyber-physical systems. Tr
 aditional techniques allow to prove some safety properties about the end s
 tate of a system\, but temporal properties are more expressive and allow t
 o express and prove properties about the interemediate states reached by t
 he 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 p
 roperties.\n\nI will then show an application to airplane collision avoida
 nce\, with a verification of the next-generation Airborne Collision Avoida
 nce System (ACASX). ACAS X is an industrial system intended to be installe
 d on all large aircraft to give advice to pilots and prevent mid-air colli
 sions with other aircraft. It is currently being developed by the Federal 
 Aviation Administration (FAA). I will determine the geometric configuratio
 ns under which the advice given by ACAS X is safe and formally verify thes
 e configurations. I will then examine the current version of the real ACAS
  X system and discuss some cases where our safety theorem conflicts with t
 he actual advisory given by that version\, demonstrating how formal\, hybr
 id approaches are helping ensure the safety of ACAS X. The approach is gen
 eral and could also be used to identify unsafe advice issued by other coll
 ision avoidance systems or confirm their safety.
LOCATION:FW26
END:VEVENT
END:VCALENDAR