Model Checking of Intersection Traffic Control Protocols

This study reports the results of model checking of two protocols that control vehicle traffic at intersections. One of the protocols uses a centralized controller that monitors and controls the vehicles at an intersection. The other one is a decentralized protocol in which vehicles communicates with each other with no centralized mechanism. We used the SPIN model checker to verify these protocols. Specifically, we check the safety property that no two vehicles enter the intersection at the same time if their routes are conflicting. As a result, we found a scenario in which the safety property can be violated for the centralized protocol. In addition, for the decentralized protocol, we detected a scenario where vehicles must wait arbitrarily long, which is a liveness error.