Deadlock Detection in the Scheduling of Last-Mile Transportation Using Model Checking
Deadlock Detection in the Scheduling of Last-Mile Transportation Using Model Checking
复制标题
DOI：
10.1109/dasc-picom-datacom-cyberscitec.2017.84
复制
发表时间：
2017-11
期刊：
影响因子：
--
通讯作者：
Koji Hasebe;Mitsuaki Tsuji;Kazuhiko Kato
中科院分区：
文献类型：
--
作者：
Koji Hasebe;Mitsuaki Tsuji;Kazuhiko Kato
针对车辆车队运行的运输系统调度问题，提出了一种死锁检测的形式化验证方法。特别是，作为一个最好的例子，我们这里考虑的是基于我们目前正在开发的自动驾驶汽车的最后一英里交通系统。我们交通系统的一大特点是车辆能够在没有物理连接点的情况下连续运行，这使得顺利重组车辆成为可能。同时，由于重新安排车队的规则和车辆的行驶路线，系统可能会陷入僵局状态，没有车辆可以进入下一站。为了解决这个问题，我们在本文中提出了一种检测给定操作计划中死锁可能性的方法。为此，我们使用模型检测方法来搜索系统的所有可能状态。我们还展示了如何根据著名的Coffman的死锁预防思想，通过修改规范来避免死锁。最后，通过实例验证了该方法的有效性。
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.