Contract-based safety verification for autonomous driving

The safe, successful deployment of autonomous systems under real-world conditions, in part, hinges upon providing rigorous performance and safety guarantees. This thesis considers the problem of establishing and verifying the safety of autonomous systems. To this end, we present a novel framework for the synthesis of safety constraints for autonomous systems, so-called safety contracts, that can be applied to and used by a wide set of real-world systems by acting as a design requirement for the controller implementation of the system. The contracts consider a large variety of road models, guarantee that the controlled system will remain safe with respect to probabilistic models of traffic behavior, and ensure that it will follow the rules of the road. We generate contracts using reachability analysis in a reach-avoid problem under consideration of dynamic obstacles, i.e., other traffic participants. Contracts are then derived directly from the reachable sets. By decomposing large road networks into local road geometries and defining assume-guarantee contracts between local geometries, we enable computational tractability over large spatial domains. To efficiently account for the behavior of other traffic participants, we iteratively alternate between falsification to generate new traffic scenarios that violate the safety contract and reachable set computation to update the safety contract. These counterexamples to collision-free behavior are found by solving a gradient-based trajectory optimization problem. We demonstrate the practical effectiveness of the proposed methods in a set of experiments involving the Manhattan road network as well as interacting multi-car traffic scenarios.

Department dc:contributor.department

Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science.

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2018

Author dc:creator

• Liebenwein, Lucas

Advisor dc:contributor.advisor

• Daniela Rus.

• Electrical Engineering and Computer Science.

Statement dc:rights

• MIT theses are protected by copyright. They may be viewed, downloaded, or printed from this source but further reproduction or distribution in any format is prohibited without written permission.

Licence dc:rights.uri

• http://dspace.mit.edu/handle/1721.1/7582

Language dc:language.iso

eng

Handle dc:identifier.uri

http://hdl.handle.net/1721.1/120366

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/120366