| Presentation | 2017-07-19 Deadlock Detection in Scheduling of Last-Mile Transportation by Using Model Checking Mitsuaki Tsuji, Koji Hasebe, Kazuhiko Kato, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | The authors are developing a last-mile transportation system with autonomous vehicles. The greatest feature is that passengers do not have to transfer by means of the way of rearrangement of fleets. On the other hand, due to the rules for rearranging fleets and the traveling route of vehicles, any vehicle may fall into a deadlock situation where it cannot proceed to the next stop. To address this problem, in this paper we propose a method to detect the possibility of 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 demonstrate the usefulness of the proposed method by using some examples. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Deadlock / Formal Method / Model Checking / Last-Mile Transportation |
| Paper # | SS2017-2,KBSE2017-2 |
| Date of Issue | 2017-07-12 (SS, KBSE) |
| Conference Information | |
| Committee | SS / KBSE / IPSJ-SE |
|---|---|
| Conference Date | 2017/7/19(3days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | Kazuhiro Ogata(JAIST) / Shigeo Kaneda(Doshisha Univ.) |
| Vice Chair | Akio Nakata(Hiroshima City Univ.) / Fumihiro Kumeno(Nippon Inst. of Tech.) |
| Secretary | Akio Nakata(Tokyo Inst. of Tech.) / Fumihiro Kumeno(Osaka Univ.) / (Kanagawa Inst. of Tech.) |
| Assistant | Kazuyuki Shima(Hiroshima City Univ.) / Takuya Saruwatari(NTT DATA) / Kosaku Kimura(Fujitsu labs.) |
| Paper Information | |
| Registration To | Technical Committee on Software Science / Technical Committee on Knowledge-Based Software Engineering / Special Interest Group on Software Engineering |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Deadlock Detection in Scheduling of Last-Mile Transportation by Using Model Checking |
| Sub Title (in English) | |
| Keyword(1) | Deadlock |
| Keyword(2) | Formal Method |
| Keyword(3) | Model Checking |
| Keyword(4) | Last-Mile Transportation |
| 1st Author's Name | Mitsuaki Tsuji |
| 1st Author's Affiliation | University of Tsukuba(Univ. of Tsukuba) |
| 2nd Author's Name | Koji Hasebe |
| 2nd Author's Affiliation | University of Tsukuba(Univ. of Tsukuba) |
| 3rd Author's Name | Kazuhiko Kato |
| 3rd Author's Affiliation | University of Tsukuba(Univ. of Tsukuba) |
| Date | 2017-07-19 |
| Paper # | SS2017-2,KBSE2017-2 |
| Volume (vol) | vol.117 |
| Number (no) | SS-136,KBSE-137 |
| Page | pp.pp.7-12(SS), pp.7-12(KBSE), |
| #Pages | 6 |
| Date of Issue | 2017-07-12 (SS, KBSE) |