Abstract
To cater for the scenario of coordinated transportation of multiple trucks on the highway, a platoon system for autonomous driving has been extensively explored in the industry. Before such a platoon is deployed, it is necessary to ensure the safety of its driving behavior, whereby each vehicle’s behavior is commanded by the decision-making function whose decision is based on the observed driving scenario. However, there is currently a lack of verification methods to ensure the reliability of the scenario-based decision-making process in the platoon system. In this paper, we focus on the platoon driving scenario, whereby the platoon is composed of intelligent heavy trucks driving on cross-sea highways. We propose a formal modeling and verification approach to provide safety assurance for platoon vehicles’ cooperative driving behaviors. The existing Multi-Lane Spatial Logic (MLSL) with a dedicated abstract model can express driving scene spatial properties and prove the safety of multi-lane traffic maneuvers under the single-vehicle perspective. To cater for the platoon system’s multi-vehicle perspective, we modify the existing abstract model and propose a Multi-Agent Spatial Logic (MASL) that extends MLSL by relative orientation and multi-agent observation. We then utilize a timed automata type supporting MASL formulas to model vehicles’ decision controllers for platoon driving. Taking the behavior of a human-driven vehicle (HDV) joining the platoon as a case study, we have implemented the model and verified safety properties on the UPPAAL tool to illustrate the viability of our framework.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Okuda R, Kajiwara Y, Terashima K. A survey of technical trend of ADAS and autonomous driving. In Proc. the 2014 International Symposium on VLSI Technology, Systems and Application, Apr. 2014. https://doi.org/10.1109/VLSITSA.2014.6839646.
Hilscher M, Linker S, Olderog E R, Ravn A P. An abstract model for proving safety of multi-lane traffic manoeuvres. In Proc. the 13th International Conference on Formal Engineering Methods, Oct. 2011, pp.404-419. https://doi.org/10.1007/978-3-642-24559-6_28.
Zita A, Mohajerani S, Fabian M. Application of formal verification to the lane change module of an autonomous vehicle. In Proc. the 13th IEEE Conference on Automation Science and Engineering, Aug. 2017, pp.932-937. https://doi.org/10.1109/COASE.2017.8256223.
Hilscher M, Schwammberger M. An abstract model for proving safety of autonomous urban traffic. In Proc. the 13th International Colloquium on Theoretical Aspects of Computing, Oct. 2016, pp.274-292. https://doi.org/10.1007/978-3-319-46750-4_16.
Xu B, Li Q. A spatial logic for modeling and verification of collision-free control of vehicles. In Proc. the 21st International Conference on Engineering of Complex Computer Systems, Nov. 2016, pp.33-42. https://doi.org/10.1109/ICECCS.2016.014.
Ro J W, Roop P S, Malik A, Ranjitkar P. A formal approach for modeling and simulation of human car-following behavior. IEEE Transactions on Intelligent Transportation Systems, 2018, 19(2): 639-648. https://doi.org/10.1109/TITS.2017.2759273.
An D, Liu J, Zhang M, Chen X, Chen M, Sun H. Uncertainty modeling and runtime verification for autonomous vehicles driving control: A machine learning-based approach. Journal of Systems and Software, 2020, 167: Article No. 110617. https://doi.org/10.1016/j.jss.2020.110617.
El-Zaher M, Gechter F, Gruer P, Hajjar M. A new linear platoon model based on reactive multi-agent systems. In Proc. the 23rd International Conference on Tools with Artificial Intelligence, Nov. 2011, pp.898-899. https://doi.org/10.1109/ICTAI.2011.146.
Kamali M, Dennis L A, Mcaree O, Fisher M, Veres S M. Formal verification of autonomous vehicle platooning. Science of Computer Programming, 2017, 148: 88-106. https://doi.org/10.1016/j.scico.2017.05.006.
Mallozzi P, Sciancalepore M, Pelliccione P. Formal verification of the on-the-fly vehicle platooning protocol. In Proc. the 13th International Workshop on Software Engineering for Resilient Systems, Sept. 2016, pp.62-75. https://doi.org/10.1007/978-3-319-45892-2_5.
Van Nguyen T, Geihs K. Formal verification of multi-agent plans for vehicle platooning. In Proc. the 9th EAI International Conference on Context-Aware Systems and Applications, and the 6th EAI International Conference on Nature of Computation and Communication, Nov. 2020, pp.3-15. https://doi.org/10.1007/978-3-030-67101-3_1.
Rashid A, Siddique U, Hasan O. Formal verification of platoon control strategies. In Proc. the 16th International Conference on Software Engineering and Formal Methods, Jun. 2018, pp.223-238. https://doi.org/10.1007/978-3-319-92970-5_14.
Peng C, Bonsangue M M, Xu Z. Model checking longitudinal control in vehicle platoon systems. IEEE Access, 2019, 7: 112015-112025. https://doi.org/10.1109/ACCESS.2019.2935423.
Alur R, Dill D. Automata for modeling real-time systems. In Proc. the 17th International Colloquium on Automata, Languages, and Programming, Jul. 1990, pp.322-335. https://doi.org/10.1007/BFb0032042.
Nyberg M, Gurov D, Lidström C, Rasmusson A, Westman J. Formal verification in automotive industry: Enablers and obstacles. In Proc. the 8th Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice, Nov. 2018, pp.139-158. https://doi.org/10.1007/978-3-030-03427-6_14.
Selvaraj Y, Ahrendt W, Fabian M. Verification of decision making software in an autonomous vehicle: An industrial case study. In Proc. the 24th Formal Methods for Industrial Critical Systems, Aug. 2019, pp.143-159. https://doi.org/10.1007/978-3-030-27008-7_9.
Todorov V, Boulanger F, Taha S. Formal verification of automotive embedded software. In Proc. the 6th International FME Workshop on Formal Methods in Software Engineering, June 2018, pp.84-87. https://doi.org/10.1145/3193992.3194003.
Sifakis J. Autonomous systems — An architectural characterization. arXiv: 1811.10277, 2018. https://arxiv.org/abs/1811.10277, Sept. 2021.
Yasmine A, Rabea A B, Patricia G O. Towards formal verification of autonomous driving supervisor functions. In Proc. the 10th European Congress on Embedded Real Time Software and Systems, Jan. 2020.
Kinoshita S, Yun S, Kitamura N, Nishimura H. Analysis of a driver and automated driving system interaction using a communicating sequential process. In Proc. the 2015 International Symposium on Systems Engineering, Sept. 2015, pp.272-277. https://doi.org/10.1109/SysEng.2015.7302769.
Brookes S D, Hoare C A R, Roscoe A W. A theory of communicating sequential processes. Journal of the ACM, 1984, 31(3): 560-599. https://doi.org/10.1145/828.833.
Roohi N, Kaur R, Weimer J, James S, Sokolsky O, Lee I. Self-driving vehicle verification towards a benchmark. arXiv: 1806.08810, 2018. https://arxiv.org/abs/18-06.08810, Sept. 2021.
Schwammberger M. Introducing liveness into multi-lane spatial logic lane change controllers using UPPAAL. Electronic Proceedings in Theoretical Computer Science, 2018, 269: 17-31. https://doi.org/10.4204/eptcs.269.3.
Xu B, Li Q. A bounded multi-dimensional modal logic for autonomous cars based on local traffic and estimation. In Proc. the 2017 International Symposium on Theoretical Aspects of Software Engineering, Sept. 2017. https://doi.org/10.1109/TASE.2017.8285637.
Xu B, Li Q, Guo T, Du D. A scenario-based approach for formal modelling and verification of safety properties in automated driving. IEEE Access, 2019, 7: 140566-14058. https://doi.org/10.1109/ACCESS.2019.2943184.
Lygeros J, Sastry S. Hybrid systems: Modeling, analysis and control. Technical Report, Electronic Research Laboratory, University of California, 2008. https://www2.eecs.berkeley.edu/Pubs/TechRpts/1999/ERL-99-34.pdf, Sept. 2021.
Alur R, Courcoubetis C, Henzinger T A, Ho P H. Hybrid Automata: An algorithmic approach to the specification and verification of hybrid systems. In Hybrid Systems, Grossman R L, Nerode A, Ravn A P, Rischel H (eds.), Springer, 1992, pp.209-229. https://doi.org/10.1007/3-540-57318-6_30.
Völker M, Kloock M, Rabanus R, Alrifaee B, Kowalewski S. Verification of cooperative vehicle behavior using temporal logic. IFAC-PapersOnLine, 2019, 52(8): 99-104. https://doi.org/10.1016/j.ifacol.2019.08.055.
Behrmann G, David A, Larsen K G. A tutorial on Uppaal. In Proc. the International School on Formal Methods for the Design of Computer, Communication, and Software Systems, Sept. 2004, pp.200-236. https://doi.org/10.1007/978-3-540-30080-9_7.
Hyun S, Song J, Shin S, Bae D H. Statistical verification framework for platooning system of systems with uncertainty. In Proc. the 26th Asia-Pacific Software Engineering Conference, Dec. 2019, pp.212-219. https://doi.org/10.1109/APSEC48747.2019.00037.
Author information
Authors and Affiliations
Corresponding author
Supplementary Information
ESM 1
(PDF 131 kb)
Rights and permissions
About this article
Cite this article
Xu, J., Huang, Y., Shi, J. et al. A Multi-Agent Spatial Logic for Scenario-Based Decision Modeling and Verification in Platoon Systems. J. Comput. Sci. Technol. 36, 1231–1247 (2021). https://doi.org/10.1007/s11390-021-1565-8
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11390-021-1565-8