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
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Bezault, E., Howard, M., Kogtenkov, A., Meyer, B., Stapf, E.: Eiffel analysis, design and programming language. ECMA International, Technical report ECMA-367 (2005)
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)
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
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)
Euro, N.: Euro NCAP 2025 roadmap: in pursuit of vision zero. Belgium, Leuven (2017)
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
Fisher, M., Dennis, L., Webster, M.: Verifying autonomous systems. Commun. ACM 56(9), 84–93 (2013)
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)
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
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
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)
Microsoft: AURIX™ 32-bit microcontrollers for automotive and industrial applications (2004). http://research.microsoft.com/en-us/projects/specsharp
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)
SAE International: Automated Driving Levels of Driving Automation are Defined in New SAE International Standard J3016 (2014). http://www.sae.org/autodrive
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
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
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
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)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
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)