Towards Formal Analysis of Vehicle Platoons Using Actor Model
2020 (English)In: IEEE International Conference on Emerging Technologies and Factory Automation, ETFA, Institute of Electrical and Electronics Engineers Inc. , 2020, p. 1820-1827Conference paper, Published paper (Refereed)
Abstract [en]
Vehicle platooning is a promising technology to save the road capacity and also fuel consumption by reducing the distance between the vehicles in the platoon. The closer the cars are to each other, the closer we are to the goals. But, this will increase the need for safety verification. In this paper we use formal methods to verify safety distance in a platoon. To do so, we present a formal actor-based model for a vehicle platoon which incorporates vehicle dynamics and communication protocol. Also, we present a method to do the analysis based on model checking that applies mathematical analysis to reduce the state space. The method uses an upper bound and a lower bound value as network delay, and verifies if a specified vehicle in a platoon has enough distance to the leader during its traveling. © 2020 IEEE.
Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers Inc. , 2020. p. 1820-1827
Keywords [en]
Actor Model, CAM, Formal Verification, Timed Rebeca, Vehicle Platoon, Factory automation, Formal methods, Vehicles, Actor-based modeling, Formal analysis, Mathematical analysis, Network delays, Safety distances, Safety verification, Vehicle dynamics, Vehicle platoons, Model checking
National Category
Embedded Systems
Identifiers
URN: urn:nbn:se:mdh:diva-52178DOI: 10.1109/ETFA46521.2020.9211888ISI: 000627406500281Scopus ID: 2-s2.0-85093360914ISBN: 9781728189567 (print)OAI: oai:DiVA.org:mdh-52178DiVA, id: diva2:1484669
Conference
25th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2020, 8 September 2020 through 11 September 2020
Note
Conference code: 163774; Export Date: 29 October 2020; Conference Paper; CODEN: 85ROA
2020-10-292020-10-292021-04-29Bibliographically approved