CMU-CS-15-144 Computer Science Department School of Computer Science, Carnegie Mellon University
Differential Refinement Logic Sarah M. Loos February 2016 Ph.D. Thesis
This thesis is focused on formal verification of cyber-physical systems. Cyberphysical systems (CPSs), such as computer-controlled cars, airplanes or robots play an increasingly crucial role in our daily lives. They are systems that we bet our lives on, so they need to be safe. However, ensuring that CPSs are safe is an intellectual challenge due to their intricate interactions of complex control software with physical behavior. Formal verification techniques, such as theorem proving, can provide strong guarantees for these systems by returning proofs that safety is preserved throughout the continuously infinite space of their possible behaviors. Previously completed work has provided: the first formal verification of distributed car control; the first formal verification of distributed, flyable, collision avoidance protocols for aircraft; and an exploration of control choices within a well-defined safety envelope. Each of these systems presented new verification challenges and required new techniques for proving safety. However, we identified a unifying hurdle for each case study that has thus far remained unaddressed: it is difficult to compare hybrid systems, even when their behaviors are very similar.
We introduce differential refinement logic (dRL), a logic with first-class
support for refinement relations on hybrid systems, and a proof calculus
for verifying such relations. The logic dRL simultaneously solves several
seemingly different challenges common in theorem proving for hybrid systems: The logic dRL extends an existing specification and verification language for hybrid systems (differential dynamic logic, dL) by adding a refinement relation to directly compare hybrid systems. This thesis gives a syntax, semantics, and proof calculus for dRL. We also demonstrate the usefulness of dRL on several examples which the author has previously completed. We show that using refinement results in easier and betterstructured proofs, leveraging as first-class citizens 131 pages
Thesis Committee:
Frank Pfenning, Head, Computer Science Department
| |
Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |