Formal Specification and Model Checking of an Autonomous Vehicle Merging Protocol
Minxuan Liu, Dang Duy Bui, Duong Dinh Tran, Kazuhiro Ogata · 2021 IEEE 21st International Conference on Software Quality, Reliability and Security Companion (QRS-C) · 2021
Self-driving/autonomous vehicles are promising transportation of the future providing many conveniences for people. Because safety is a point of paramount significance for any autonomous vehicle system, a large number of researchers have proposed mechanisms/protocols to automatically control vehicles running on public roads without any collision. S. Aoki and R. Rajkumar proposed a merging protocol for autonomous vehicles. The protocol controls autonomous vehicles running on two one-way lanes (one through lane and one non-through lane) such that such vehicles pass through the merge point without any collision. The protocol uses real-time information, such as the average speed of multiple vehicles running on a lane. We have revised the protocol such that it never uses such information because the speeds of vehicles may drastically change in a short moment. We have then formally specified the revised version of the protocol in Maude and conducted some model checking experiments with Maude that the revised version enjoys some desired properties.