Toward a Driver's License Test for Robotic Cars
| Table of Contents |
|---|
How to Prove Your Car Correct
Cars are prime examples of safety-critical cyber-physical systems. They move physically as they drive down the road, and they are subject to discrete decisions as a phletora of embedded devices, computers, and driver assistance technology help control the car safely. A number of experiments have shown quite impressively that computer control can help a lot, both as local driver assistance technology as well as in the form of full-fledged autononmous driving. In either scenario, computers hold a lot of promise in making driving safer and reducing the risks, the hazzle, and the inefficiencies in today's transportation situations.
One big challenge in putting any of those systems into productive and reliable use is the question how to make sure that the cars will operate safer with automatic control than they would without. That is why one of the goals of that we pursue is to develop a driver's license test for robotic cars.
Driver's License Test for Robotic Cars
Every human has to pass a driver's license before we let them loose on the road. But how could we conduct a driver's license test for robotic cars? Is this a simple test where the robotic car has to drive around the block once? Would we trust it, if it succeeded? Would we be sure that it can handle all other situations as well? Actually not. We would not be sure with humans either, whether they can manage the next challenging situation at the next intersection as well. But humans are pretty amazing, flexible, and adaptive beings, who learn to master new situations surprisingly quickly. Admittedly, humans still make mistakes. But would we accept a robotic car that makes mistakes systematically? Would you want a broken robotic car drive next to you on the road? Would you trust a robotic car with your life if you sit in it and read your newspaper instead of watching the road?
What makes developing a driver's license test for robotic cars particularly difficult is the fact that, for principle reasons, this cannot just work like a driver's license test for humans. No matter how difficult the test course is that one uses for a robotic driver's license test, there are algorithms that pass this test, but still make many systematic mistakes in other scenarios How can one possibly ever distinguish the controller of a safe robot car from an algorithm that was just lucky passing the particular test course and would fail in nearly all other real-world situations? This is a very difficult question (in fact, undecidable). Just trying a ever more complicated obstacle courses would not be enough.
Logic to the Rescue
In this research, we take a much more fundamental approach and develop techniques with whic we can systematically prove whether a robotic car will always do what it should. This research uses logic, proofs, and mathematics to figure that out. In fact, in this research project, we do not even focus exclusively on fully autonomous robotic cars, but develop techniques that also work in driver assistance technology, or any embedded systems challenge in cars, or even in other systems.
For example, the following formula in differential dynamic logic (dL) expresses that for the state of the car controllers of a local lane controller llc, the follower car f is always safely behind the leader car l when starting in a state where f is already safely behind l:
For a fair number of aspects of car control, distributed car control, local control, and traffic center car interaction control, we have already found good answers and have developed provably safe controllers and system models:
|
 |
 |
 |
 |
 |
 |
In the News
Many sources have publicized our work, demonstrating the public and societal demand for safety in the technologies of the future. While some of these reports have exaggerated the results of our research, we do believe that our work is an important step toward safer vehicles and safer technology.
Read about this research in the news.
ScienceNews for Kids |
Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified
Car safety measures can be most effective when the cars on a street coordinate their control actions using distributed cooperative control. While each car optimizes its navigation planning locally to ensure the driver reaches his destination, all cars coordinate their actions in a distributed way in order to minimize the risk of safety hazards and collisions. These systems control the physical aspects of car movement using cyber technologies like local and remote sensor data and distributed V2V and V2I communication. They are thus cyber-physical systems. In this paper, we consider a distributed car control system that is inspired by the ambitions of the California PATH project, the CICAS system, SAFESPOT and PReVENT initiatives. We develop a formal model of a distributed car control system in which every car is controlled by adaptive cruise control. One of the major technical difficulties is that faithful models of distributed car control have both distributed systems and hybrid systems dynamics. They form distributed hybrid systems, which makes them very challenging for verification. In a formal proof system, we verify that the control model satisfies its main safety objective and guarantees collision freedom for arbitrarily many cars driving on a street, even if new cars enter the lane from on-ramps or multi-lane streets. The system we present is in many ways one of the most complicated cyber-physical systems that has ever been fully verified formally.
Keywords: Distributed car control, Multi-agent systems, Highway traffic safety, Formal verification, Distributed hybrid systems, Adaptive cruise control
Selected Publications
Also see publications on verification of automotive systems.
-
Stefan Mitsch, Khalil Ghorbal, David Vogelbacher, and André Platzer.
Formal verification of obstacle avoidance and navigation of ground robots.
International Journal of Robotics Research 36(12), pp. 1312-1340, 2017. © The authors
[bib | ⧉ | pdf | doi | kyx | arXiv | abstract]
-
Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger and André Platzer.
A component-based approach to hybrid systems safety verification.
In Erika Abraham and Marieke Huisman, editors, Integrated Formal Methods - 12th International Conference, iFM 2016, Reykjavik, Iceland, June 1-4, 2016, Proceedings, volume 9681 of LNCS, pp. 441-456. Springer, 2016. © Springer
[bib | ⧉ | pdf | doi | slides | TR | abstract]
-
Andreas Müller and Stefan Mitsch and André Platzer.
Verified traffic networks: Component-based verification of cyber-physical flow systems.
In Intelligent Transportation Systems ITSC'15', IEEE 18th International Conference on, pp. 757-764, 2015. © IEEE
[bib | ⧉ | pdf | doi | slides | abstract]
-
Sarah M. Loos, David Witmer, Peter Steenkiste and André Platzer.
Efficiency analysis of formally verified adaptive cruise controllers.
In Andreas Hegyi and Bart De Schutter, editors, 16th International IEEE Conference on Intelligent Transportation Systems, ITSC'13, The Hague, Netherlands, Proceedings, 2013. © IEEE
[bib | ⧉ | pdf | doi | slides | study | abstract]
-
André Platzer.
The complete proof theory of hybrid systems.
ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pp. 541-550. IEEE 2012. © IEEE
[bib | ⧉ | pdf | doi | slides | TR | abstract]
-
Stefan Mitsch, Sarah M. Loos and André Platzer.
Towards formal verification of freeway traffic control.
In Chenyang Lu, editor, ACM/IEEE Third International Conference on Cyber-Physical Systems ICCPS'12, Beijing, China, April 17-19. pp. 171-180, IEEE. 2012. © IEEE
[bib | ⧉ | pdf | doi | slides | study | abstract]
-
Nikos Aréchiga, Sarah M. Loos, André Platzer and Bruce H. Krogh.
Using theorem provers to guarantee closed-loop system properties.
In Dawn Tilbury, editor, American Control Conference, ACC'12, Montréal, Canada, June 27-29. pp. 3573-3580. 2012. © IEEE
[bib | ⧉ | pdf | doi | abstract]
-
Sarah M. Loos and André Platzer.
Safe intersections: At the crossing of hybrid systems and verification.
In Kyongsu Yi, editor, 14th International IEEE Conference on Intelligent Transportation Systems, ITSC'11, Washington, DC, USA, Proceedings, pp. 1181-1186. 2011. © IEEE
[bib | ⧉ | pdf | doi | slides | study | abstract]
-
Sarah M. Loos, André Platzer and Ligia Nistor.
Adaptive cruise control:
Hybrid, distributed, and now formally verified.
In Michael Butler and Wolfram Schulte, editors, 17th International Symposium on Formal Methods, FM, Limerick, Ireland, Proceedings, volume 6664 of LNCS, pp. 42-56. Springer, 2011. © Springer
[bib | ⧉ | pdf | doi | slides | study | TR | abstract]
-
Sarah M. Loos, André Platzer and Ligia Nistor.
Adaptive Cruise Control:
Hybrid, Distributed, and Now Formally Verified.
School of Computer Science, Carnegie Mellon University, CMU-CS-11-107, 2011.
[bib | ⧉ | pdf | FM'10]
-
André Platzer.
Quantified differential invariants.
In Emilio Frazzoli and Radu Grosu, editors, Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, USA, April 12-14, pp. 63-72. ACM, 2011. © ACM
[bib | ⧉ | pdf | doi | slides | abstract]
-
André Platzer.
A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems.
Logical Methods in Computer Science 8(4), pp. 1-44, 2012.
Special issue for selected papers from CSL'10. © The author
[bib | ⧉ | pdf | doi | arXiv | CSL'10 | abstract]
-
André Platzer.
Quantified differential dynamic logic for distributed hybrid systems.
In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 19th EACSL Annual Conference, CSL 2010, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247 of LNCS, pp. 469-483. Springer, 2010. © Springer
[bib | ⧉ | pdf | doi | slides | TR | LMCS'12 | abstract]
-
André Platzer.
Differential dynamic logic for hybrid systems.
Journal of Automated Reasoning 41(2), pp. 143-189, 2008. © The author
[bib | ⧉ | pdf | doi | mypdf | study | abstract]
 |
Any opinions, findings, and conclusions or recommendations expressed are those of the author(s) and do not necessarily reflect the views of any sponsoring institution.