salle A. Turing CE4
7 November 2014 - 14h00
Differential Temporal Dynamic Logic for Hybrid Systems and Airplane Collision Avoidance
by Jean-Baptiste Jeannin from Carnegie Mellon University
Abstract: Differential Dynamic Logic can express important properties about
Cyber-Physical Systems, by combining discrete assignments and control
structures with differential equations. However it can only express
properties about the end state of a system. In this talk, we first
introduce the differential temporal dynamic logic dTL2, a logic to
specify properties about the intermediate states reached by a hybrid
system. It combines differential dynamic logic with temporal logic,
and supports some linear time temporal properties of LTL. It extends
differential temporal dynamic logic dTL with nested temporalities. We
provide a semantics and a proof system for the logic dTL2, and show
its usefulness for nontrivial temporal properties of hybrid
systems. We take particular care to handle the case of alternating
universal dynamic and existential temporal modalities and its dual,
solving an open problem formulated in previous work.
We 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). We determine
the geometric configurations under which the advice given by ACAS X is
safe under a precise set of assumptions and formally verify these
configurations. We conduct an initial examination of 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. Our approach is general and could also be
used to identify unsafe advice issued by other collision avoidance
systems or confirm their safety.
