@techreport{oai:ipsj.ixsq.nii.ac.jp:00226911,
 author = {Masaki, Nakamura and Tatsuya, Igarashi and Yifan, Wang and Kazutoshi, Sakakibara and Masaki, Nakamura and Tatsuya, Igarashi and Yifan, Wang and Kazutoshi, Sakakibara},
 issue = {7},
 month = {Jul},
 note = {The Lim-Jeong-Park-Lee protocol (LJPL protocol) has been proposed as an efficient distributed mutual exclusion algorithm for intersection traffic control, which manages a queue of vehicles to enter the intersection. In our previous work, we have verified its safety property by using the timed OTS/CafeOBJ method in a macro level. In this study, we model an autonomous vehicle control system of the queue as a micro level of LJPL protocol, where a vehicle can enter the intersection even if the vehicle in front is still crossing it under some time constraints. We describe a formal specification of the model and verify its safety property by the timed OTS/CafeOBJ method., The Lim-Jeong-Park-Lee protocol (LJPL protocol) has been proposed as an efficient distributed mutual exclusion algorithm for intersection traffic control, which manages a queue of vehicles to enter the intersection. In our previous work, we have verified its safety property by using the timed OTS/CafeOBJ method in a macro level. In this study, we model an autonomous vehicle control system of the queue as a micro level of LJPL protocol, where a vehicle can enter the intersection even if the vehicle in front is still crossing it under some time constraints. We describe a formal specification of the model and verify its safety property by the timed OTS/CafeOBJ method.},
 title = {Formal verification of an autonomous vehicle control system by the timed OTS/CafeOBJ method},
 year = {2023}
}