Cyber-physical systems (CPSs) combining discrete control and continuous physical dynamics are pervasive in modern society: examples include driver assistance in cars, industrial robotics, airborne collision avoidance systems, and the electrical grid. Many of these systems are safety-critical because they operate in close proximity to humans. Formal safety verification of these systems is important because it is a key tool for attaining the strongest possible safety guarantees.

Hybrid systems models, in particular, are a successful formalism for CPS. Hybrid systems theorem-proving in differential dynamic logic (dL) and its generalization differential game logic (dGL) are notable for strong logical foundations and successful application in case studies using the theorem provers KeYmaera and KeYmaera X. However, safety verification of models does not imply safety of implementations, which might not be faithful to the model. Moreover, a machine-checked proof is only as trustworthy as the software which checks it, thus correctness of proof-checkers is crucial.

This thesis addresses implementation and soundness gaps by using constructive logic and programming languages as the foundation of an end-to-end verification toolchain. That is: Constructive Differential Game Logic (CdGL) enables practical, end-to-end verification of cyber-physical systems. CdGL enables synthesis of implementations with bulletproof theoretical foundations. Logic is the keystone of the end-to-end connection from high-level proofs and foundations to implementations. Our pursuit of practical proving includes innovations in the proof language itself.

CdGL proofs, in contrast to dGL, are suitable for synthesizing controllers which determine safe actions for a CPS and monitors which check the compliance of the external environment with model assumptions. The synthesized code is automatically proven correct down to machine-code level. The foundations are also strengthened by our formalization of classical dL's soundness in Isabelle/HOL, allowing hybrid systems proofs in dL to be exported and rechecked. We evaluate the toolchain on a 2D robot which follows arcs. The model and implementation cross-validate each other: monitors catch incorrect code and assumptions, while testing with monitors enabled allows us to assess the realism of the model.

581 pages

Thesis Committee:
André Platzer (Chair)
Stefan Mitsch
Frank Pfenning
Bradley Schmerl
Tobias Nipkow (Technical University Munich)

Srinivasan Seshan, Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu