We propose a formal verification method for deadlock detection in the scheduling of transportation systems in which vehicles run in fleets. Especially, as a prime example, we here consider the last-mile transportation system based on autonomous vehicles that we are currently developing. One of the major features of our transportation system is the ability for vehicles to run in a row without physical connecting points, which makes it possible to smoothly reorganize the vehicles. Meanwhile, owing to the rules for rearranging fleets and the traveling route of vehicles, the system may fall into a deadlock state where no vehicle can proceed to the next stop. To address this issue, we propose in this paper a method of detecting the possibility of a deadlock in a given operation schedule. For this objective, we use a model checking method to search all possible states of the system. We also show how to avoid deadlock by modifying specification based on the well-known idea of Coffman's deadlock prevention. Finally, we demonstrate the usefulness of the proposed method using examples.
Deadlock Detection in the Scheduling of Last-Mile Transportation Using Model Checking
2017-11-01
287588 byte
Conference paper
Electronic Resource
English
Routing and Scheduling for a Last-Mile Transportation System
British Library Online Contents | 2019
|