Compositional and Contract-based Verification for Autonomous Driving on Road Networks

Recent advances in autonomous driving have raised the problem of safety to the forefront and incentivized research into establishing safety guarantees. In this paper, we propose a safety verification framework as a safety standard for driving controllers with full or shared autonomy based on composi...

Full description

Bibliographic Details
Main Authors: DeCastro, Jonathan (Author), Alonso-Mora, Javier (Author), Liebenwein, Lucas (Contributor), Schwarting, Wilko (Contributor), Vasile, Cristian-Ioan (Contributor), Karaman, Sertac (Contributor), Rus, Daniela L (Contributor)
Other Authors: Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory (Contributor), Massachusetts Institute of Technology. Department of Aeronautics and Astronautics (Contributor), Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science (Contributor), Massachusetts Institute of Technology. Department of Mechanical Engineering (Contributor), Rus, Daniela (Contributor)
Format: Article
Language:English
Published: International Foundation of Robotics Research, 2018-03-14T15:52:04Z.
Subjects:
Online Access:Get fulltext
LEADER 02719 am a22003373u 4500
001 114151
042 |a dc 
100 1 0 |a DeCastro, Jonathan  |e author 
100 1 0 |a Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory  |e contributor 
100 1 0 |a Massachusetts Institute of Technology. Department of Aeronautics and Astronautics  |e contributor 
100 1 0 |a Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science  |e contributor 
100 1 0 |a Massachusetts Institute of Technology. Department of Mechanical Engineering  |e contributor 
100 1 0 |a Rus, Daniela  |e contributor 
100 1 0 |a Liebenwein, Lucas  |e contributor 
100 1 0 |a Schwarting, Wilko  |e contributor 
100 1 0 |a Vasile, Cristian-Ioan  |e contributor 
100 1 0 |a Karaman, Sertac  |e contributor 
100 1 0 |a Rus, Daniela L  |e contributor 
700 1 0 |a Alonso-Mora, Javier  |e author 
700 1 0 |a Liebenwein, Lucas  |e author 
700 1 0 |a Schwarting, Wilko  |e author 
700 1 0 |a Vasile, Cristian-Ioan  |e author 
700 1 0 |a Karaman, Sertac  |e author 
700 1 0 |a Rus, Daniela L  |e author 
245 0 0 |a Compositional and Contract-based Verification for Autonomous Driving on Road Networks 
260 |b International Foundation of Robotics Research,   |c 2018-03-14T15:52:04Z. 
856 |z Get fulltext  |u http://hdl.handle.net/1721.1/114151 
520 |a Recent advances in autonomous driving have raised the problem of safety to the forefront and incentivized research into establishing safety guarantees. In this paper, we propose a safety verification framework as a safety standard for driving controllers with full or shared autonomy based on compositional and contract-based principles. Our framework enables us to synthesize safety guarantees over entire road networks by first building a library of locally verified models, and then composing local models together to verify the entire network. Composition is achieved using assume-guarantee contracts that are synthesized concurrently during verification. Thus, we can reuse local models within and across networks, add additional models to cover local road geometries without re-verifying the entire library, and perform all computations in a parallel and distributed way, which enables computational tractability. Furthermore, we employ controller contracts such that any controller satisfying them can be certified safe. We demonstrate the practical effectiveness of our framework by certifying controllers over parts of the Manhattan road network. Keywords: Verification, Safety, Autonomous Car, Composition, Contracts 
546 |a en_US 
655 7 |a Article 
773 |t 2017 International Symposium on Robotics Research (ISRR)