Skip to main content
SpringerLink
Log in

A Formally Verified Motion Planner for Autonomous Vehicles

  • Conference paper
  • First Online:
Book cover Automated Technology for Verification and Analysis (ATVA 2018)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11138))

Abstract

Autonomous vehicles are safety-critical cyber-physical systems. To ensure their correctness, we use a proof assistant to prove safety properties deductively. This paper presents a formally verified motion planner based on manoeuvre automata in Isabelle/HOL. Two general properties which we ensure are numerical soundness (the absence of floating-point errors) and logical correctness (satisfying a plan specified in linear temporal logic). From these two properties, we obtain a motion planner whose correctness only depends on the validity of the models of the ego vehicle and its environment.

A. Rizaldi and B. Schürmann—This work is partially supported by the DFG Graduiertenkolleg 1840 (PUMA) and the European Comission project UnCoVerCPS under grant number 643921.

F. Immler—Supported by DFG Koselleck grant NI 491/16-1. Moreover, this material is based upon work supported by the Air Force Office of Scientific Research under grant number FA9550-18-1-0120. Any opinions, finding, and conclusion or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the United States Air Force.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    The formalisation is in https://gitlab.lrz.de/ga96tej/manoeuvre-automata.

  2. 2.

    From now on, ‘Isabelle’ refers to ‘Isabelle/HOL’ for simplicity.

  3. 3.

    Yu’s formalisation was inspired by Harrison’s [18] extensive formalisation in HOL Light. More work on floating-point numbers in theorem provers has been done in the comprehensive formalisation of floating-point numbers by Boldo and Melquiond [9] in Coq as well as early efforts in ACL2 [26].

  4. 4.

    For high-dimensional zonotopes, please consult the technique described in CORA [1].

References

  1. Althoff, M.: An introduction to CORA 2015. In: Proceedings of the Workshop on Applied Verification for Continuous and Hybrid Systems (2015)

    Google Scholar 

  2. Althoff, M., Grebenyuk, D.: Implementation of interval arithmetic in CORA 2016. In: Proceedings of the 3rd International Workshop on Applied Verification for Continuous and Hybrid Systems, pp. 91–105 (2016)

    Google Scholar 

  3. Althoff, M., Koschi, M., Manzinger, S.: CommonRoad: composable benchmarks for motion planning on roads. In: Proceedings of the IEEE Intelligent Vehicles Symposium, pp. 719–726 (2017)

    Google Scholar 

  4. Anand, A., Knepper, R.A.: ROSCoq: robots powered by constructive reals. In: Proceedings of the 6th International Conference on Interactive Theorem Proving, pp. 34–50 (2015)

    Google Scholar 

  5. Belta, C., Bicchi, A., Egerstedt, M., Frazzoli, E., Klavins, E., Pappas, G.J.: Symbolic planning and control of robot motion [grand challenges of robotics]. IEEE Robot. Autom. Mag. 14(1), 61–70 (2007)

    Article  Google Scholar 

  6. Belta, C., Isler, V., Pappas, G.J.: Discrete abstractions for robot motion planning and control in polygonal environments. IEEE Trans. Robot. 21(5), 864–874 (2005)

    Article  Google Scholar 

  7. Berz, M., Makino, K.: Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models. Reliab. Comput. 4(4), 361–369 (1998)

    Article  MathSciNet  Google Scholar 

  8. Bohrer, B., Tan, Y.K., Mitsch, S., Myreen, M., Platzer, A.: Veriphy: Verified controller executables from verified cyber-physical system models. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (2018). https://doi.org/10.1145/3192366.3192406

  9. Boldo, S., Melquiond, G.: Flocq: a unified library for proving floating-point algorithms in Coq. In: Proceedings of the IEEE Computer Arithmetic Symposium, pp. 243–252 (2011)

    Google Scholar 

  10. Egerstedt, M.B., Brockett, R.W.: Feedback can reduce the specification complexity of motor programs. IEEE Trans. Autom. Control 48(2), 213–223 (2003)

    Article  MathSciNet  Google Scholar 

  11. Fainekos, G.E., Kress-Gazit, H., Pappas, G.J.: Temporal logic motion planning for mobile robots. In: Proceedings of the IEEE International Conference on Robotics and Automation, pp. 2020–2025 (2005)

    Google Scholar 

  12. Fainekos, G.E., Girard, A., Kress-Gazit, H., Pappas, G.J.: Temporal logic motion planning for dynamic robots. Automatica 45(2), 343–352 (2009)

    Article  MathSciNet  Google Scholar 

  13. de Figueiredo, L., Stolfi, J.: Affine arithmetic: concepts and applications. Numer. Algorithms 37(1–4), 147–158 (2004)

    Article  MathSciNet  Google Scholar 

  14. Frazzoli, E., Dahleh, M.A., Feron, E.: Maneuver-based motion planning for nonlinear systems with symmetries. IEEE Trans. Robot. 21(6), 1077–1091 (2005)

    Article  Google Scholar 

  15. Fulton, N., Mitsch, S., Quesel, J.-D., Völp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 527–538. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_36

    Chapter  Google Scholar 

  16. Gavrilets, V., Mettler, B., Feron, E.: Human-inspired control logic for automated maneuvering of miniature helicopter. J. Guidance Control Dyn. 27(5), 752–759 (2004)

    Article  Google Scholar 

  17. Guibas, L.J., Nguyen, A., Zhang, L.: Zonotopes as bounding volumes. In: Proceedings of the Fourteenth Annual ACM-SIAM Symposium on Discrete Algorithms, pp. 803–812 (2003)

    Google Scholar 

  18. Harrison, J.: Floating-point verification using theorem proving. In: Proceedings of the 6th International Conference on Formal Methods for the Design of Computer, Communication, and Software Systems, pp. 211–242 (2006)

    Chapter  Google Scholar 

  19. Hölzl, J.: Proving inequalities over reals with computation in Isabelle/HOL. In: Proceedings of the ACM International Workshop on Programming Languages for Mechanized Mathematics Systems, pp. 38–45 (2009)

    Google Scholar 

  20. Immler, F.: Formally verified computation of enclosures of solutions of ordinary differential equations. In: Proceedings of the 6th International Symposium of NASA Formal Methods, pp. 113–127 (2014)

    Google Scholar 

  21. Immler, F.: A verified algorithm for geometric zonotope/hyperplane intersection. In: Proceedings of International Conference on Certified Programs and Proofs, pp. 129–136 (2015)

    Google Scholar 

  22. Immler, F.: Verified reachability analysis of continuous systems. In: Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 37–51 (2015)

    Google Scholar 

  23. Krauss, A.: Automating recursive definitions and termination proofs in higher-order logic, Ph.D. thesis, Technical University Munich (2009)

    Google Scholar 

  24. Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 179–191 (2014)

    Google Scholar 

  25. Mitsch, S., Ghorbal, K., Vogelbacher, D., Platzer, A.: Formal verification of obstacle avoidance and navigation of ground robots. Int. J. Robot. Res. 36(12), 1312–1340 (2017)

    Article  Google Scholar 

  26. Moore, J.S., Lynch, T., Kaufmann, M.: A mechanically checked proof of the correctness of the kernel of the AMD5K86 floating-point division algorithm. IEEE Trans. Comput. 47(9), 913–926 (1996)

    Article  Google Scholar 

  27. Moore, R.E.: Methods and Applications of Interval Analysis. SIAM, Philadelphia (1979)

    Book  Google Scholar 

  28. Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9

    Book  MATH  Google Scholar 

  29. Obua, S.: Flyspeck II: The Basic Linear Programs, Ph.D. thesis, Technische Universität München, München (2008)

    Google Scholar 

  30. Plaku, E., Kavraki, L.E., Vardi, M.Y.: Falsification of LTL safety properties in hybrid systems. Int. J. Softw. Tools Technol. Transf. 15(4), 305–320 (2013)

    Article  Google Scholar 

  31. Platzer, A.: Differential dynamic logic for hybrid systems. J. Automa. Reason. 41(2), 143–189 (2008)

    Article  MathSciNet  Google Scholar 

  32. Rizaldi, A., Keinholz, J., Huber, M., Feldle, J., Immler, F., Althoff, M., Hilgendorf, E., Nipkow, T.: Formalising traffic rules for autonomous vehicles involving multiple lanes in Isabelle/HOL. In: Proceedings of the 13th International Conference on integrated Formal Methods, pp. 50–66 (2017)

    Google Scholar 

  33. Roehm, H., Oehlerking, J., Heinz, T., Althoff, M.: STL model checking of continuous and hybrid systems. In: Proceedings of 14th International Symposium on Automated Technology for Verification and Analysis, pp. 412–427 (2016)

    Chapter  Google Scholar 

  34. Rump, S.M., Kashiwagi, M.: Implementation and improvements of affine arithmetic. Nonlinear Theory Appl. IEICE 6(3), 341–359 (2015)

    Article  Google Scholar 

  35. Schürmann, B., Althoff, M.: Convex interpolation control with formal guarantees for disturbed and constrained nonlinear systems. In: Proceedings of the Hybrid Systems: Computation and Control, pp. 121–130 (2017)

    Google Scholar 

  36. Schürmann, B., Heß, D., Eilbrecht, J., Stursberg, O., Köster, F., Althoff, M.: Ensuring drivability of planned motions using formal methods. In: Proceedings of the Intelligent Transportation Systems Conference, pp. 1661–1668 (2017)

    Google Scholar 

  37. Yu, L.: A formal model of IEEE floating point arithmetic. Arch. Form. Proofs (2018). http://isa-afp.org/entries/IEEE_Floating_Point.html. ISSN: 2150-914x

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Technische Universität München, Munich, Germany

    Albert Rizaldi, Bastian Schürmann & Matthias Althoff

  2. Computer Science Department, Carnegie Mellon University, Pittsburgh, USA

    Fabian Immler

Authors
  1. Albert Rizaldi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fabian Immler
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Bastian Schürmann
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Matthias Althoff
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Albert Rizaldi .

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, WA, USA

    Shuvendu K. Lahiri

  2. University of Southern California, Los Angeles, CA, USA

    Chao Wang

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Rizaldi, A., Immler, F., Schürmann, B., Althoff, M. (2018). A Formally Verified Motion Planner for Autonomous Vehicles. In: Lahiri, S., Wang, C. (eds) Automated Technology for Verification and Analysis. ATVA 2018. Lecture Notes in Computer Science(), vol 11138. Springer, Cham. https://doi.org/10.1007/978-3-030-01090-4_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-01090-4_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-01089-8

  • Online ISBN: 978-3-030-01090-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation