A Case Study on Formally Validating Motion Rules for Autonomous Cars | SpringerLink
Skip to main content

A Case Study on Formally Validating Motion Rules for Autonomous Cars

  • Conference paper
  • First Online:
Software Engineering and Formal Methods. SEFM 2020 Collocated Workshops (SEFM 2020)

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

Included in the following conference series:

  • 653 Accesses

Abstract

Car motion control is a key functional stage for providing advanced assisted or autonomous driving capabilities to vehicles. Car motion is subject to strict safety rules which are normally expressed in natural language. As such, these natural language rules are subject to potential misinterpretation during the implementation phase of the motion control stage. In this paper, we show a novel approach by which safety rules are expressed in natural language, then in a formal language specification which is then validated and used to generate a car motion checker. We present a case study of using the approach with true road capture data and its associated imperfections. We also show how the approach lowers the validation efforts needed to guarantee that the car motion always respects a desired set of safety rules while other traditional validation methods would be much heavier to deploy and error prone.

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

Access this chapter

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • 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

Similar content being viewed by others

References

  1. Bezault, E., Howard, M., Kogtenkov, A., Meyer, B., Stapf, E.: Eiffel analysis, design and programming language. ECMA International, Technical report ECMA-367 (2005)

    Google Scholar 

  2. De Waen, J., Dinh, H.T., Cruz Torres, M.H., Holvoet, T.: Scalable multirotor UAV trajectory planning using mixed integer linear programming. In: 2017 European Conference on Mobile Robots (ECMR), pp. 1–6 (2017)

    Google Scholar 

  3. Dinh, H.T., Cruz Torres, M.H., Holvoet, T.: Dancing uavs: Using linear programming to model movement behavior with safety requirements. In: International Conference on Unmanned Aircraft Systems, pp. 326–335. IEEE (2017). https://doi.org/10.1109/ICUAS.2017.7991352. https://lirias.kuleuven.be/1571693

  4. Dinh, H.T., Cruz Torres, M.H., Holvoet, T.: Combining planning and model checking to get guarantees on the behavior of safety-critical UAV systems. In: ICAPS Workshop on Planning and Robotics. ICAPS Workshop on Planning and Robotics (2018)

    Google Scholar 

  5. Euro, N.: Euro NCAP 2025 roadmap: in pursuit of vision zero. Belgium, Leuven (2017)

    Google Scholar 

  6. European Commission: Revision of the EU General Safety Regulation and Pedestrian Safety Regulation (2018). https://www.unece.org/fileadmin/DAM/trans/doc/2018/wp29grsp/GRSP-63-31e.pdf

  7. Fisher, M., Dennis, L., Webster, M.: Verifying autonomous systems. Commun. ACM 56(9), 84–93 (2013)

    Article  Google Scholar 

  8. Giacalone, J., Bourgeois, L., Ancora, A.: Challenges in aggregation of heterogeneous sensors for autonomous driving systems. In: 2019 IEEE Sensors Applications Symposium (SAS), pp. 1–5 (2019)

    Google Scholar 

  9. Gu, R., Marinescu, R., Seceleanu, C., Lundqvist, K.: Towards a two-layer framework for verifying autonomous vehicles. In: Badger, J.M., Rozier, K.Y. (eds.) NASA Formal Methods, pp. 186–203. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-20652-9_12

    Chapter  Google Scholar 

  10. Infineon: AURIX™ 32-bit microcontrollers for automotive and industrial applications (2020). https://www.unece.org/fileadmin/DAM/trans/doc/2018/wp29grsp/GRSP-63-31e.pdf

  11. Maoz, S., Ringert, J.O.: Gr (1) synthesis for LTL specification patterns. In: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, pp. 96–106 (2015)

    Google Scholar 

  12. Microsoft: AURIX™ 32-bit microcontrollers for automotive and industrial applications (2004). http://research.microsoft.com/en-us/projects/specsharp

  13. Pek, C., Koschi, M., Althoff, M.: An online verification framework for motion planning of self-driving vehicles with safety guarantees. In: AAET-Automatisiertes und vernetztes Fahren (2019)

    Google Scholar 

  14. SAE International: Automated Driving Levels of Driving Automation are Defined in New SAE International Standard J3016 (2014). http://www.sae.org/autodrive

  15. Schwarting, W., Alonso-Mora, J., Rus, D.: Planning and decision-making for autonomous vehicles. Annual Rev. Control, Robot. Autonom. Syst. 1(1), 187–210 (2018). https://doi.org/10.1146/annurev-control-060117-105157

  16. Shalev-Shwartz, S., Shammah, S., Shashua, A.: On a formal model of safe and scalable self-driving cars. CoRR abs/1708.06374 (2017). http://arxiv.org/abs/1708.06374

  17. Wolff, E.M., Murray, R.M.: Optimal control of nonlinear systems with temporal logic specifications. In: Inaba, M., Corke, P. (eds.) Robotics Research. STAR, vol. 114, pp. 21–37. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-28872-7_2

    Chapter  Google Scholar 

  18. Wongpiromsarn, T., Topcu, U., Ozay, N., Xu, H., Murray, R.M.: Tulip: a software toolbox for receding horizon temporal logic planning. In: Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control, pp. 313–314 (2011)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Joelle Abou Faysal .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Torres, M.H.C., Giacalone, JP., Abou Faysal, J. (2021). A Case Study on Formally Validating Motion Rules for Autonomous Cars. In: Cleophas, L., Massink, M. (eds) Software Engineering and Formal Methods. SEFM 2020 Collocated Workshops. SEFM 2020. Lecture Notes in Computer Science(), vol 12524. Springer, Cham. https://doi.org/10.1007/978-3-030-67220-1_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-67220-1_18

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-67219-5

  • Online ISBN: 978-3-030-67220-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics