Final research report

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

PDF

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.

US Transportation Collection

DTRT12GUTG11