Advertisement

Formalising and Monitoring Traffic Rules for Autonomous Vehicles in Isabelle/HOL

  • Albert RizaldiEmail author
  • Jonas Keinholz
  • Monika Huber
  • Jochen Feldle
  • Fabian Immler
  • Matthias Althoff
  • Eric Hilgendorf
  • Tobias Nipkow
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10510)

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.

References

  1. 1.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14:1–14:64 (2011)CrossRefGoogle Scholar
  3. 3.
    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)Google Scholar
  4. 4.
    Bundesgerichtshof: Sorgfaltspflichten beim überholen auf der autobahn, pp. 481–482. Neue Juristische Wochenschrift: NJW (1954)Google Scholar
  5. 5.
    Burmann, M., Heß, R., Hühnermann, K., Jahnke, J., Janker, H.: Straßenverkehrsrecht: Kommentar, 24th edn. C.H. Beck (2016)Google Scholar
  6. 6.
    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)Google Scholar
  7. 7.
    Gutt, S.: Gesamtes Verkehrsrecht, 1st edn. Nomos (2014)Google Scholar
  8. 8.
    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 CrossRefGoogle Scholar
  9. 9.
    Hentschel, P., König, P., Dauer, P.: Straßenverkehrsrecht: Kommentar, 43rd edn. C.H. Beck (2015)Google Scholar
  10. 10.
    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)Google Scholar
  11. 11.
    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)Google Scholar
  12. 12.
    Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View. Texts in Theoretical Computer Science. EATCS Series, 2nd edn. Springer, Heidelberg (2016)CrossRefzbMATHGoogle Scholar
  13. 13.
    Küster, J.C.: Runtime verification on data-carrying traces. Ph.D. thesis, The Australian National University, October 2016Google Scholar
  14. 14.
    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 CrossRefGoogle Scholar
  15. 15.
    Oberlandesgericht Karlsruhe: Gefährdung des Nachfolgendes beim Überholen. Neue Zeitschrift für Verkehrsrecht (NZV), pp. 248–249 (1992)Google Scholar
  16. 16.
    Park, S.C., Shin, H.: Polygonal chain intersection. Comput. Graph. 26(2), 341–350 (2002)CrossRefGoogle Scholar
  17. 17.
    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)Google Scholar
  18. 18.
    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 CrossRefGoogle Scholar
  19. 19.
    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)CrossRefGoogle Scholar
  20. 20.
    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)Google Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • Albert Rizaldi
    • 1
    Email author
  • Jonas Keinholz
    • 1
  • Monika Huber
    • 1
  • Jochen Feldle
    • 2
  • Fabian Immler
    • 1
  • Matthias Althoff
    • 1
  • Eric Hilgendorf
    • 2
  • Tobias Nipkow
    • 1
  1. 1.Institut für InformatikTechnische Universität MünchenMunichGermany
  2. 2.Forschungsstelle RobotRechtJulius-Maximilians-Universität WürzburgWürzburgGermany

Personalised recommendations