Abstract
Recent accidents involving autonomous vehicles prompt us to consider how we can engineer an autonomous vehicle which always obeys traffic rules. This is particularly challenging because traffic rules are rarely specified at the level of detail an engineer would expect. Hence, it is nearly impossible to formally monitor behaviours of autonomous vehicles—which are expressed in terms of position, velocity, and acceleration—with respect to the traffic rules—which are expressed by vague concepts such as “maintaining safe distance”. We show how we can use the Isabelle theorem prover to do this by first codifying the traffic rules abstractly and then subsequently concretising each atomic proposition in a verified manner. Thanks to Isabelle’s code generation, we can generate code which we can use to monitor the compliance of traffic rules formally.
A. Rizaldi—This work is partially supported by the DFG Graduiertenkolleg 1480 (PUMA), DFG NI 491/16-1, European Commission project UnCoVerCPS 643921.
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
Notes
- 1.
Our Isabelle formalisation is in https://github.com/rizaldialbert/overtaking.
- 2.
We also have similar theorems for decrease-lane but they are omitted for brevity.
- 3.
This can be checked in our Isabelle formalisation.
- 4.
The semantics for LTL is pretty standard and, hence, we omit them for brevity.
References
Basin, D.A., Klaedtke, F., Müller, S., Zalinescu, E.: Monitoring metric first-order temporal properties. J. ACM 62(2), 15:1–15:45 (2015)
Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14:1–14:64 (2011)
Bender, P., Ziegler, J., Stiller, C.: Lanelets: efficient map representation for autonomous driving. In: Proceedings of the IEEE Intelligent Vehicles Symposium, Michigan, MI, USA, pp. 420–425 (2014)
Bundesgerichtshof: Sorgfaltspflichten beim überholen auf der autobahn, pp. 481–482. Neue Juristische Wochenschrift: NJW (1954)
Burmann, M., Heß, R., Hühnermann, K., Jahnke, J., Janker, H.: Straßenverkehrsrecht: Kommentar, 24th edn. C.H. Beck (2016)
Giannakopoulo, D., Havelund, K.: Automata-based verification of temporal properties on running programs. In: Proceedings of the 16th Annual International Conference on Automated Software Engineering (ASE), San Diego, CA, USA, pp. 412–416 (2001)
Gutt, S.: Gesamtes Verkehrsrecht, 1st edn. Nomos (2014)
Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 103–117. Springer, Heidelberg (2010). doi:10.1007/978-3-642-12251-4_9
Hentschel, P., König, P., Dauer, P.: Straßenverkehrsrecht: Kommentar, 43rd edn. C.H. Beck (2015)
Hölzl, J.: Proving inequalities over reals with computation in Isabelle/HOL. In: Proceedings of the ACM SIGSAM International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS 2009), Munich, pp. 38–45 (2009)
Immler, F.: A verified algorithm for geometric zonotope/hyperplane intersection. In: Proceedings of the International Conference on Certified Programs and Proofs (CPP), Mumbai, India, pp. 129–136 (2015)
Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View. Texts in Theoretical Computer Science. EATCS Series, 2nd edn. Springer, Heidelberg (2016)
Küster, J.C.: Runtime verification on data-carrying traces. Ph.D. thesis, The Australian National University, October 2016
Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT -2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30206-3_12
Oberlandesgericht Karlsruhe: Gefährdung des Nachfolgendes beim Überholen. Neue Zeitschrift für Verkehrsrecht (NZV), pp. 248–249 (1992)
Park, S.C., Shin, H.: Polygonal chain intersection. Comput. Graph. 26(2), 341–350 (2002)
Rizaldi, A., Althoff, M.: Formalising traffic rules for accountability of autonomous vehicles. In: Proceedings of the 18th IEEE International Conference on Intelligent Transportation Systems, Las Palmas de Gran Canaria Canary Islands, Spain, pp. 1658–1665 (2015)
Rizaldi, A., Immler, F., Althoff, M.: A formally verified checker of the safe distance traffic rules for autonomous vehicles. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 175–190. Springer, Cham (2016). doi:10.1007/978-3-319-40648-0_14
Sergot, M.J., Sadri, F., Kowalski, R.A., Kriwaczek, F., Hammond, P., Cory, H.T.: The British Nationality Act as a logic program. Commun. ACM 29(5), 370–386 (1986)
Werling, M., Ziegler, J., Kammel, S., Thrun, S.: Optimal trajectory generation for dynamic street scenarios in a frenet frame. In: Proceedings of the IEEE International Conference on Robotics and Automation, Anchorage, AK, USA, pp. 987–993 (2010)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Rizaldi, A. et al. (2017). Formalising and Monitoring Traffic Rules for Autonomous Vehicles in Isabelle/HOL. In: Polikarpova, N., Schneider, S. (eds) Integrated Formal Methods. IFM 2017. Lecture Notes in Computer Science(), vol 10510. Springer, Cham. https://doi.org/10.1007/978-3-319-66845-1_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-66845-1_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66844-4
Online ISBN: 978-3-319-66845-1
eBook Packages: Computer ScienceComputer Science (R0)