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:

1. When hybrid systems are complicated, it is useful to prove properties about simpler and related subsystems before tackling the system as a whole.
2. Some models of hybrid systems can be implementation-specific. Verification can be aided by abstracting the system down to the core components necessary for safety, but only if the relations between the abstraction and the original system can be guaranteed.
3. One approach to taming the complexities of hybrid systems is to start with a simplified version of the system, prove it safe, and then iteratively expand it. However, this approach can be costly, since every iteration has to be proved safe from scratch, unless refinement relations can be leveraged in the proof.
4. When proofs become large, it is difficult to maintain a modular or comprehensile proof structure. By using a refinement relation to arrange proofs hierarchically according to the structure of natural subsystems, we can increase the readability, modularity, and reusability of the resulting proof.

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:
André Platzer (Chair)
Frank Pfenning
Dexter Kozen (Cornell University)
Stefan Mitsch (Johannes Kepler University Linz)
George Pappas (University of Pennsylvania)

Frank Pfenning, Head, Computer Science Department
Andrew W. Moore, Dean, School of Computer Science

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu