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 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.
-
Format:
-
Funding:
-
Collection(s):
-
Main Document Checksum:
-
Download URL:
-
File Type: