Towards Formal Analysis of Vehicle Platoons Using Actor Model

• 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.

Ämnesord

TEKNIK OCH TEKNOLOGIER  -- Elektroteknik och elektronik -- Inbäddad systemteknik (hsv//swe)

ENGINEERING AND TECHNOLOGY  -- Electrical Engineering, Electronic Engineering, Information Engineering -- Embedded Systems (hsv//eng)

Nyckelord

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

Publikations- och innehållstyp

ref (ämneskategori)

kon (ämneskategori)