Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
DeepSafe: A Data-Driven Approach for Assessing Robustness of Neural Networks Kapitel lesen Erstes Kapitel lesen

2018 | OriginalPaper | Buchkapitel

A Formally Verified Motion Planner for Autonomous Vehicles

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

Erschienen in: Automated Technology for Verification and Analysis

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel What’s to Come is Still Unsure
Nächstes Kapitel Robustness Testing of Intermediate Verifiers
Fußnoten
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].
 
Literatur
1.
Althoff, M.: An introduction to CORA 2015. In: Proceedings of the Workshop on Applied Verification for Continuous and Hybrid Systems (2015)
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)
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)
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)
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)CrossRef
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)CrossRef
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)MathSciNetCrossRef
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)
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)MathSciNetCrossRef
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)
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)MathSciNetCrossRef
13.
de Figueiredo, L., Stolfi, J.: Affine arithmetic: concepts and applications. Numer. Algorithms 37(1–4), 147–158 (2004)MathSciNetCrossRef
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)CrossRef
15.
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)CrossRef
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)
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)CrossRef
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)
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)
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)
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)
23.
Krauss, A.: Automating recursive definitions and termination proofs in higher-order logic, Ph.D. thesis, Technical University Munich (2009)
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)
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)CrossRef
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)CrossRef
27.
Moore, R.E.: Methods and Applications of Interval Analysis. SIAM, Philadelphia (1979)CrossRef
28.
29.
Obua, S.: Flyspeck II: The Basic Linear Programs, Ph.D. thesis, Technische Universität München, München (2008)
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)CrossRef
31.
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)
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)CrossRef
34.
Rump, S.M., Kashiwagi, M.: Implementation and improvements of affine arithmetic. Nonlinear Theory Appl. IEICE 6(3), 341–359 (2015)CrossRef
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)
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)
37.
Metadaten
Titel
A Formally Verified Motion Planner for Autonomous Vehicles
verfasst von
Albert Rizaldi
Fabian Immler
Bastian Schürmann
Matthias Althoff
Copyright-Jahr
2018
Buch
Automated Technology for Verification and Analysis

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

Electronic ISBN: 978-3-030-01090-4

Copyright-Jahr: 2018

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