Overview of Logical Foundations of Cyber-Physical Systems

TL;DR

This paper reviews the logical foundations of cyber-physical systems, emphasizing differential dynamic logic and its implementation in KeYmaera X for verifying safety in complex hybrid systems.

Contribution

It provides an overview of the logical approach to CPS safety, highlighting the use of differential dynamic logic and theorem proving in verifying hybrid system controllers.

Findings

Verified controllers for ground robots, railway systems, and ACAS X.

Demonstrated safety guarantees from verified models to actual CPS execution.

Showcased the effectiveness of KeYmaera X in formal verification.

Abstract

Cyber-physical systems (CPSs) are important whenever computer technology interfaces with the physical world as it does in self-driving cars or aircraft control support systems. Due to their many subtleties, controllers for cyber-physical systems deserve to be held to the highest correctness standards. Their correct functioning is crucial, which explains the broad interest in safety analysis technology for their mathematical models, which are called hybrid systems because they combine discrete dynamics with continuous dynamics. Differential dynamic logic (dL) provides logical specification and rigorous reasoning techniques for hybrid systems. The logic dL is implemented in the theorem prover KeYmaera X, which has been instrumental in verifying ground robot controllers, railway systems, and the next-generation airborne collision avoidance system ACAS X. This chapter provides an informal overview of this logical approach to CPS safety that is detailed in a recent textbook on Logical Foundations of Cyber-Physical Systems. It also explains how safety guarantees obtained in the land of verified models reach the level of CPS execution unharmed.