Abstract
Autonomous Driving Systems (ADS) are critical dynamic reconfigurable agent systems whose specification and validation raises extremely challenging problems. The paper presents a multilevel semantic framework for the specification of ADS and discusses associated validation problems. The framework relies on a formal definition of maps modeling the physical environment in which vehicles evolve. Maps are directed metric graphs whose nodes represent positions and edges represent segments of roads. We study basic properties of maps including their geometric consistency. Furthermore, we study position refinement and segment abstraction relations allowing multilevel representation from purely topological to detailed geometric. We progressively define first order logics for modeling families of maps and distributions of vehicles over maps. These are Configuration Logics, which in addition to the usual logical connectives are equipped with a coalescing operator to build configurations of models. We study their semantics and basic properties. We illustrate their use for the specification of traffic rules and scenarios characterizing sequences of scenes. We study various aspects of the validation problem including run-time verification and satisfiability of specifications. Finally, we show links of our framework with practical validation needs for ADS and advocate its adequacy for addressing the many facets of this challenge.
Institute of Engineering Univ. Grenoble Alpes.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
the derivative \(\dot{c}\) exists and is continuous on [0, 1].
- 2.
the instantaneous speed \({|\dot{c}|}\), that is, the Euclidean norm of the derivative is constant.
- 3.
every edge occurs at most once in the path.
- 4.
Except if needed for encoding the length of segment types.
References
ASAM OpenDRIVE® - open dynamic road information for vehicle environment. Technical report, V 1.6.0, ASAM e.V., Mar 2020. https://www.asam.net/standards/detail/opendrive
ASAM OpenScenario® - dynamic content in driving simulation, UML modeling rules. Technical report, V 1.0.0, ASAM e.V., Mar 2020. https://www.asam.net/standards/detail/openscenario
Bagschik, G., Menzel, T., Maurer, M.: Ontology based scene creation for the development of automated vehicles. In: Intelligent Vehicles Symposium, pp. 1813–1820. IEEE (2018)
El Ballouli, R., Bensalem, S., Bozga, M., Sifakis, J.: Four exercises in programming dynamic reconfigurable systems: methodology and solution in DR-BIP. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11246, pp. 304–320. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03424-5_20
Beetz, J., Borrmann, A.: Benefits and limitations of linked data approaches for road modeling and data exchange. In: Smith, I., Domer, B. (eds.) EG-ICE 2018. LNCS, vol. 10864, pp. 245–261. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-91638-5_13
Bozga, M., Sifakis, J.: Specification and validation of autonomous driving systems: a multilevel semantic framework. CoRR abs/2109.06478 (2021). https://arxiv.org/abs/2109.06478
Chen, W., Kloul, L.: An ontology-based approach to generate the advanced driver assistance use cases of highway traffic. In: KEOD, pp. 73–81. SciTePress (2018)
Damm, W., Kemper, S., Möhlmann, E., Peikenkamp, T., Rakow, A.: Using traffic sequence charts for the development of HAVs. In: ERTS 2018, Proceedings (2018)
Dosovitskiy, A., Ros, G., Codevilla, F., López, A.M., Koltun, V.: CARLA: an open urban driving simulator. In: Proceedings of Machine Learning Research, vol. 78, pp. 1–16. PMLR (2017). CoRL
El-Hokayem, A., Bozga, M., Sifakis, J.: A temporal configuration logic for dynamic reconfigurable systems. In: SAC, pp. 1419–1428. ACM (2021)
Esterle, K., Aravantinos, V., Knoll, A.C.: From specifications to behavior: maneuver verification in a semantic state space. In: IV, pp. 2140–2147. IEEE (2019)
Esterle, K., Gressenbuch, L., Knoll, A.C.: Formalizing traffic rules for machine interpretability. In: CAVS, pp. 1–7. IEEE (2020)
Fremont, D.J., et al.: Scenic: a language for scenario specification and data generation. CoRR abs/2010.06580 (2020). https://arxiv.org/abs/2010.06580
Fremont, D.J., et al.: Formal scenario-based testing of autonomous vehicles: from simulation to the real world. In: ITSC, pp. 1–8. IEEE (2020)
Harel, D., Marron, A., Sifakis, J.: Autonomics: in search of a foundation for next-generation autonomous systems. Proc. Natl. Acad. Sci. USA 117(30), 17491–17498 (2020)
Hilscher, M., Linker, S., Olderog, E.-R., Ravn, A.P.: An abstract model for proving safety of multi-lane traffic manoeuvres. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 404–419. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24559-6_28
Institute for Software Engineering and Programming Languages, University of Lübeck: LamaConv - Logics and Automata Converter Library (2020). https://www.isp.uni-luebeck.de/lamaconv
Karimi, A., Duggirala, P.S.: Formalizing traffic rules for uncontrolled intersections. In: ICCPS, pp. 41–50. IEEE (2020)
Poggenhans, F., et al.: Lanelet2: a high-definition map framework for the future of automated driving. In: ITSC, pp. 1672–1679. IEEE (2018)
Rizaldi, A., Althoff, M.: Formalising traffic rules for accountability of autonomous vehicles. In: ITSC, pp. 1658–1665. IEEE (2015)
Rizaldi, A., Immler, F., Schürmann, B., Althoff, M.: A formally verified motion planner for autonomous vehicles. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 75–90. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-01090-4_5
Rizaldi, A., et al.: Formalising and monitoring traffic rules for autonomous vehicles in Isabelle/HOL. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 50–66. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66845-1_4
Rong, G., et al.: LGSVL simulator: a high fidelity simulator for autonomous driving. CoRR abs/2005.03778 (2020). https://arxiv.org/abs/2005.03778
Schönemann, V., et al.: Scenario-based functional safety for automated driving on the example of valet parking. In: Arai, K., Kapoor, S., Bhatia, R. (eds.) FICC 2018. AISC, vol. 886, pp. 53–64. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-03402-3_5
Sifakis, J.: Autonomous systems – an architectural characterization. In: Boreale, M., Corradini, F., Loreti, M., Pugliese, R. (eds.) Models, Languages, and Tools for Concurrent and Distributed Programming. LNCS, vol. 11665, pp. 388–410. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-21485-2_21
Wikipedia. https://en.wikipedia.org/wiki/All-way_stop
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Bozga, M., Sifakis, J. (2022). Specification and Validation of Autonomous Driving Systems: A Multilevel Semantic Framework. In: Raskin, JF., Chatterjee, K., Doyen, L., Majumdar, R. (eds) Principles of Systems Design. Lecture Notes in Computer Science, vol 13660. Springer, Cham. https://doi.org/10.1007/978-3-031-22337-2_5
Download citation
DOI: https://doi.org/10.1007/978-3-031-22337-2_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-22336-5
Online ISBN: 978-3-031-22337-2
eBook Packages: Computer ScienceComputer Science (R0)