Verifying distributed car and aircraft systems with logic and refinement

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. 

Sarah Loos is a Ph.D. student in the computer science department at Carnegie Mellon University. Her research interests include logical analysis and formal verification of distributed hybrid systems, such as distributed car control and collision avoidance protocols for aircraft. She is a Department of Energy computational science graduate fellow and an NSF graduate research fellow. In addition to her role as co-editor of the ACM-W newsletter, Sarah has served as a student member on the board of trustees and board of advisors for the Anita Borg Institute for Women and Technology.  She currently serves on the board of directors for the Foundation for Learning Equality, a non-profit tech company dedicated to bringing the online learning revolution to communities with little or no internet connectivity.  Sarah received her undergraduate B.S. degrees in computer science and math from Indiana University.