Tech Report

United States

Final research report

Carnegie-Mellon University. Technologies for Safe and Efficient Transportation University Transportation Center

The main objective of this project was to provide technology for answering crucial safety and correctness questions about verification of autonomous vehicle and advanced driver assistance systems based on logic. In synergistic activities, we have significantly improved tooling for cyber physical systems (CPS) verification, including the development of the completely new theorem prover KeYmaera X [7] based on a uniform substitution calculus for differential dynamic logic. This project saw a substantial advance in the foundation of proof certificates by developing the logic of proof for differential dynamic logic (LPdL) [8] as a foundation for CPS safety certificates. This report briefly explains the key benefits of KeYmaera X over existing systems that are relevant for the goals of this project and discusses the advances that LPdL bring in detail. LPdL answers the key question of safety evidence for autonomous vehicles and driver assistance safety technology or other cyber-physical systems: What counts as undeniable mathematical evidence in support of a safety claim for an autonomous vehicle or advanced safety critical driver assistance technology? Without any doubt mathematical evidence for safety claims of these systems will differ from classical mathematical evidence, because the safety argument some how has to take both the relevant features of the computer control into account together with an analysis of its impact on the motion of the vehicle. Such safety evidence is inherently about dynamics not about static situations. LPdL gives first-class access to safety properties and their safety certificates as proof terms. It extends both the syntax and semantics of differential dynamic logic (dL), the logic for hybrid system models of cyber physical systems, with proof terms as syntactic representations of logical deductions that serve as theoretically well-founded evidence or certificates for the truth of the safety claim they prove. To support axiomatic theorem proving,the logic allows equivalence rewriting deep within formulas and supports both uniform renaming and uniform substitutions. In addition to serving as unambiguous proof certificates, LPdL also advances KeYmaera X in there major points: (1) provide a clean separation between proof checking and proof search; (2) implement a mechanism for composing, reusing, or parameterizing proofs (merely mechanisms for composing provability); (3) take advantage of procedures that require interrogating or modifying the structure of a proof. Models of cyber-physical systems are of ten stated as non-deterministic programs because a non-deterministic model can capture a variety of environmental conditions and a variety of control decisions. For example, a car’s sensors might sample at non-deterministic points in time, and its control program might choose between acceleration and deceleration in ways that are not known a priori (or that are overly laborious to specify during verification). Synthesizing a most-conservative deterministic controller from these non-deterministic models plugs a major remaining gap between CPS models and control software implementations. LPdL directly prepares for a supports of this goal in a way that truth-preserving operations cannot.

PDF

DTRT12GUTG11

US Transportation Collection