United States Department of Transportation
ROSA P serves as an archival repository of USDOT-published products including scientific findings, journal articles, guidelines, recommendations, or other information authored or co-authored by USDOT or funded partners.
As a repository, ROSA P retains documents in their original published format to ensure public access to scientific information.
i
Proving Autonomous Vehicle and Advanced Driver Assistance Systems Safety: Final Research Report
-
2016-02-15
-
Details:
-
Creators:
-
Corporate Creators:
-
Corporate Contributors:
-
Subject/TRT Terms:
-
Resource Type:
-
Geographical Coverage:
-
Edition:Final research report
-
Corporate Publisher:
-
Abstract: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 somehow 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 often 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 support of this goal in a way that truth-preserving operations cannot.
-
Format:
-
Funding:
-
Collection(s):
-
Main Document Checksum:
-
Download URL:
-
File Type:
[PDF-851.47 KB]
