Formal methods and theorem proving have been used successfully in many discrete applications, such as chip design and verification, but computation is not confined to the discrete world. Increasingly, we depend on discrete software to control safety-critical components of continuous physical systems. It is vital that these hybrid (discrete and continuous) systems behave as designed or they will cause more damage than they intend to fix. In this talk, I will present several challenges associated with verifying hybrid systems and how we use differential dynamic logics to ensure safety for hybrid systems under a continuously infinite range of circumstances and unbounded time horizon.
I will discuss the first formal proof of safety for a distributed car control system and the first formal verification of distributed, flyable, collision-avoidance protocols for aircraft. In both cases, our verification holds for an unbounded number of cars or aircraft, so the systems are protected against unexpected emergent behavior, which simulation and testing may miss.
Providing the first formal proofs of these systems required the development of several seemingly unrelated techniques. We have since identified a unifying challenge for each case study: It is difficult to compare hybrid systems, even when their behaviors are very similar. I will discuss the development of a logic with first-class support for refinement relations on hybrid systems, called differential refinement logic, which aims to address this core challenge for hybrid systems verification within a formal framework.
