Skip to main content
SpringerLink
Log in

A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles

  • Conference paper
  • First Online:
NASA Formal Methods (NFM 2016)

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

Included in the following conference series:

Abstract

One barrier in introducing autonomous vehicle technology is the liability issue when these vehicles are involved in an accident. To overcome this, autonomous vehicle manufacturers should ensure that their vehicles always comply with traffic rules. This paper focusses on the safe distance traffic rule from the Vienna Convention on Road Traffic. Ensuring autonomous vehicles to comply with this safe distance rule is problematic because the Vienna Convention does not clearly define how large a safe distance is. We provide a formally proved prescriptive definition of how large this safe distance must be, and correct checkers for the compliance of this traffic rule. The prescriptive definition is obtained by: (1) identifying all possible relative positions of stopping (braking) distances; (2) selecting those positions from which a collision freedom can be deduced; and (3) reformulating these relative positions such that lower bounds of the safe distance can be obtained. These lower bounds are then the prescriptive definition of the safe distance, and we combine them into a checker which we prove to be sound and complete. Not only does our work serve as a specification for autonomous vehicle manufacturers, but it could also be used to determine who is liable in court cases and for online verification of autonomous vehicles’ trajectory planner.

A. Rizaldi and F. Immler—Supported by the DFG Graduiertenkolleg 1480 (PUMA)

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 54.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.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.

    Our formalisation is available at http://home.in.tum.de/~immler/safedistance/index.html

  2. 2.

    NGSIM has identified the other vehicle for each ego vehicle in the US-101 Highway data set.

  3. 3.

    We use Lagrange’s notation \(f'\) and \(f''\) to denote the first and the second derivative of f.

References

  1. Aghabayk, K., Sarvi, M., Young, W.: A state-of-the-art review of car-following models with particular considerations of heavy vehicles. Transport Rev. 35(1), 82–105 (2015)

    Article  Google Scholar 

  2. Althoff, M., Dolan, J.: Online verification of automated road vehicles using reachability analysis. IEEE Trans. Robot. 30(4), 903–918 (2014)

    Article  Google Scholar 

  3. American Prosecutors Research Institute: Crash Reconstruction Basics for Prosecutors: Targeting Hardcore Impaired Drivers. Author (2003)

    Google Scholar 

  4. Chen, C., Liu, L., Du, X., Pei, Q., Zhao, X.: Improving driving safety based on safe distance design in vehicular sensor networks. Int. J. Distrib. Sens. Netw. 2012(469067), 13 (2012)

    Google Scholar 

  5. Eberl, M.: A decision procedure for univariate real polynomials in Isabelle/HOL. In: Proceedings of the 2015 Conference on Certified Programs and Proofs. CPP 2015, Mumbai, India, pp. 75–83. ACM, New York (2015). http://doi.acm.org/10.1145/2676724.2693166

  6. Fricke, L.: Traffic Accident Reconstruction. The Traffic Accident Investigation Manual, vol. 2, Northwestern University Center for Public Safety (1990)

    Google Scholar 

  7. Gipps, P.: A behavioural car-following model for computer simulation. Transp. Res. B Methodological 15(2), 105–111 (1981)

    Article  Google Scholar 

  8. Goodloe, A.E., Muñoz, C., Kirchner, F., Correnson, L.: Verification of numerical programs: from real numbers to floating point numbers. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 441–446. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  9. Haftmann, F., Krauss, A., Kunčar, O., Nipkow, T.: Data refinement in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 100–115. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  10. 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)

    Chapter  Google Scholar 

  11. Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 102–118. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  12. 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. pp. 38–45 (2009)

    Google Scholar 

  13. Immler, F.: Verified reachability analysis of continuous systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 37–51. Springer, Heidelberg (2015)

    Google Scholar 

  14. Kowshik, H., Caveney, D., Kumar, P.: Provable systemwide safety in intelligent intersections. IEEE Trans. Veh. Technol. 60(3), 804–818 (2011)

    Article  Google Scholar 

  15. Loos, S.M., Platzer, A., Nistor, L.: Adaptive cruise control: hybrid, distributed, and now formally verified. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 42–56. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  16. Loos, S., Platzer, A.: Safe intersections: at the crossing of hybrid systems and verification. In: IEEE Conference on Intelligent Transportations Systems. pp. 1181–1186, October 2011

    Google Scholar 

  17. McLaughlin, S., Harrison, J.V.: A proof-producing decision procedure for real arithmetic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 295–314. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  18. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  19. Olsen, R.A.: Pedestrian injury issues in litigation. In: Karwowski, W., Noy, Y.I. (eds.) Handbook of Human Factors in Litigation, pp. 15-1–15-23. CRC Press, Boca Raton (2004)

    Google Scholar 

  20. Platzer, A.: Logical Analysis of Hybrid Systems. Springer, Heidelberg (2010)

    Book  MATH  Google Scholar 

  21. Platzer, A.: A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems. Logical Methods Comput. Sci. 8(4), 1–44 (2012)

    MathSciNet  MATH  Google Scholar 

  22. Qu, D., Chen, X., Yang, W., Bian, X.: Modeling of car-following required safe distance based on molecular dynamics. Math. Probl. Eng. 2014(604023), 7 (2014)

    Google Scholar 

  23. Rizaldi, A., Althoff, M.: Formalising traffic rules for accountability of autonomous vehicles. In: IEEE Conference on Intelligent Transportation Systems. pp. 1658–1665 (2015)

    Google Scholar 

  24. Vanholme, B., Gruyer, D., Lusetti, B., Glaser, S., Mammar, S.: Highly automated driving on highways based on legal safety. IEEE Trans. Intell. Transp. Syst. 14(1), 333–347 (2013)

    Article  Google Scholar 

  25. Wilson, B.H.: How soon to brake and how hard to brake: unified analysis of the envelope of opportunity for rear-end collision warnings. In: Enhanced Safety of Vehicles. vol. 47 (2001)

    Google Scholar 

  26. Xiao, L., Gao, F.: A comprehensive review of the development of adaptive cruise control systems. Veh. Syst. Dyn. 48(10), 1167–1192 (2010)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Albert Rizaldi, Fabian Immler & Matthias Althoff

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. 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. University of Minnesota, Minneapolis, Minnesota, USA

    Sanjai Rayadurgam

  2. NASA Ames Research Center , Moffett Field, California, USA

    Oksana Tkachuk

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Rizaldi, A., Immler, F., Althoff, M. (2016). A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles. In: Rayadurgam, S., Tkachuk, O. (eds) NASA Formal Methods. NFM 2016. Lecture Notes in Computer Science(), vol 9690. Springer, Cham. https://doi.org/10.1007/978-3-319-40648-0_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-40648-0_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-40647-3

  • Online ISBN: 978-3-319-40648-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation