Skip to main content
Top

2018 | OriginalPaper | Chapter

A Formally Verified Motion Planner for Autonomous Vehicles

Authors : Albert Rizaldi, Fabian Immler, Bastian Schürmann, Matthias Althoff

Published in: Automated Technology for Verification and Analysis

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
2
From now on, ‘Isabelle’ refers to ‘Isabelle/HOL’ for simplicity.
 
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
For high-dimensional zonotopes, please consult the technique described in CORA [1].
 
Literature
1.
go back to reference Althoff, M.: An introduction to CORA 2015. In: Proceedings of the Workshop on Applied Verification for Continuous and Hybrid Systems (2015) Althoff, M.: An introduction to CORA 2015. In: Proceedings of the Workshop on Applied Verification for Continuous and Hybrid Systems (2015)
2.
go back to reference 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) 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)
3.
go back to reference 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) 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)
4.
go back to reference 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) 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)
5.
go back to reference 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)CrossRef 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)CrossRef
6.
go back to reference 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)CrossRef 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)CrossRef
7.
go back to reference 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)MathSciNetCrossRef 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)MathSciNetCrossRef
8.
go back to reference 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 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.
go back to reference 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) 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)
10.
go back to reference Egerstedt, M.B., Brockett, R.W.: Feedback can reduce the specification complexity of motor programs. IEEE Trans. Autom. Control 48(2), 213–223 (2003)MathSciNetCrossRef Egerstedt, M.B., Brockett, R.W.: Feedback can reduce the specification complexity of motor programs. IEEE Trans. Autom. Control 48(2), 213–223 (2003)MathSciNetCrossRef
11.
go back to reference 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) 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)
12.
go back to reference Fainekos, G.E., Girard, A., Kress-Gazit, H., Pappas, G.J.: Temporal logic motion planning for dynamic robots. Automatica 45(2), 343–352 (2009)MathSciNetCrossRef Fainekos, G.E., Girard, A., Kress-Gazit, H., Pappas, G.J.: Temporal logic motion planning for dynamic robots. Automatica 45(2), 343–352 (2009)MathSciNetCrossRef
13.
go back to reference de Figueiredo, L., Stolfi, J.: Affine arithmetic: concepts and applications. Numer. Algorithms 37(1–4), 147–158 (2004)MathSciNetCrossRef de Figueiredo, L., Stolfi, J.: Affine arithmetic: concepts and applications. Numer. Algorithms 37(1–4), 147–158 (2004)MathSciNetCrossRef
14.
go back to reference Frazzoli, E., Dahleh, M.A., Feron, E.: Maneuver-based motion planning for nonlinear systems with symmetries. IEEE Trans. Robot. 21(6), 1077–1091 (2005)CrossRef Frazzoli, E., Dahleh, M.A., Feron, E.: Maneuver-based motion planning for nonlinear systems with symmetries. IEEE Trans. Robot. 21(6), 1077–1091 (2005)CrossRef
16.
go back to reference 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)CrossRef 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)CrossRef
17.
go back to reference 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) 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)
18.
go back to reference 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)CrossRef 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)CrossRef
19.
go back to reference 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) 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)
20.
go back to reference 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) 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)
21.
go back to reference Immler, F.: A verified algorithm for geometric zonotope/hyperplane intersection. In: Proceedings of International Conference on Certified Programs and Proofs, pp. 129–136 (2015) Immler, F.: A verified algorithm for geometric zonotope/hyperplane intersection. In: Proceedings of International Conference on Certified Programs and Proofs, pp. 129–136 (2015)
22.
go back to reference 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) 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)
23.
go back to reference Krauss, A.: Automating recursive definitions and termination proofs in higher-order logic, Ph.D. thesis, Technical University Munich (2009) Krauss, A.: Automating recursive definitions and termination proofs in higher-order logic, Ph.D. thesis, Technical University Munich (2009)
24.
go back to reference 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) 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)
25.
go back to reference 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)CrossRef 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)CrossRef
26.
go back to reference 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)CrossRef 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)CrossRef
27.
go back to reference Moore, R.E.: Methods and Applications of Interval Analysis. SIAM, Philadelphia (1979)CrossRef Moore, R.E.: Methods and Applications of Interval Analysis. SIAM, Philadelphia (1979)CrossRef
29.
go back to reference Obua, S.: Flyspeck II: The Basic Linear Programs, Ph.D. thesis, Technische Universität München, München (2008) Obua, S.: Flyspeck II: The Basic Linear Programs, Ph.D. thesis, Technische Universität München, München (2008)
30.
go back to reference 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)CrossRef 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)CrossRef
32.
go back to reference 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) 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)
33.
go back to reference 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)CrossRef 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)CrossRef
34.
go back to reference Rump, S.M., Kashiwagi, M.: Implementation and improvements of affine arithmetic. Nonlinear Theory Appl. IEICE 6(3), 341–359 (2015)CrossRef Rump, S.M., Kashiwagi, M.: Implementation and improvements of affine arithmetic. Nonlinear Theory Appl. IEICE 6(3), 341–359 (2015)CrossRef
35.
go back to reference 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) 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)
36.
go back to reference 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) 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)
Metadata
Title
A Formally Verified Motion Planner for Autonomous Vehicles
Authors
Albert Rizaldi
Fabian Immler
Bastian Schürmann
Matthias Althoff
Copyright Year
2018
DOI
https://doi.org/10.1007/978-3-030-01090-4_5

Premium Partner