VeriPhy: verified controller executables from verified cyber-physical system models

Abstract

We present VeriPhy, a verified pipeline which automatically transforms verified high-level models of safety-critical cyber-physical systems (CPSs) in differential dynamic logic (dL) to verified controller executables. VeriPhy proves that all safety results are preserved end-to-end as it bridges abstraction gaps, including: i) the gap between mathematical reals in physical models and machine arithmetic in the implementation, ii) the gap between real physics and its differential-equation models, and iii) the gap between nondeterministic controller models and machine code. VeriPhy reduces CPS safety to the faithfulness of the physical environment, which is checked at runtime by synthesized, verified monitors. We use three provers in this effort: KeYmaera X, HOL4, and Isabelle/HOL. To minimize the trusted base, we cross-verify KeYmaeraX in Isabelle/HOL. We evaluate the resulting controller and monitors on commodity robotics hardware.

Document Details

Document Type
Pub Defense Publication
Publication Date
Jun 11, 2018
Source ID
10.1145/3296979.3192406

Entities

People

  • AndrĂ© Platzer
  • Magnus O. Myreen
  • Rose Bohrer
  • Stefan Mitsch
  • Yong Kiam Tan

Organizations

  • Air Force Office of Scientific Research
  • Carnegie Mellon University
  • Chalmers University of Technology
  • Defense Advanced Research Projects Agency
  • National Science Foundation

Tags

Fields of Study

  • Computer science

Readers

  • Mathematical Modeling and Probability Theory.
  • Robotics and Automation.
  • Software Engineering.

Technology Areas

  • AI & ML
  • AI & ML - Autonomous Systems
  • AI & ML - Machine Learning Algorithms
  • Autonomy
  • Autonomy - Autonomous System Control
  • Cyber