CMU-CS-21-115.pdf (4.96 MB)
Download file

Practical End-to-End Verification of Cyber-Physical Systems

Download (4.96 MB)
posted on 03.08.2022, 20:03 authored by Rose Bohrer

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.


Automatic Recognition and Understanding of the Driving Environment for Driver Feedback

United States Department of Transportation

Find out more...

DOD DTRT57-15-D-30011

NSF CNS1054246

NSF CNS1739629

Air Force FA87501220291

Provably Secure Cyber-Physical Systems

United States Air Force

Find out more...




Degree Type



Computer Science

Degree Name

  • Doctor of Philosophy (PhD)


André Platzer