| Presentation | 2021-03-15 Model Checking-Based Verification of Token-Based Traffic Control for Roundabouts Tatsuhiro Tsuchiya, Satoshi Otsuka, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | This paper reports the results of model checking-based verification of a traffic control mechanism for roundabouts. This mechanism controls cars in a roundabout by transferring electronic tokens between the cars and the gates located at the entrances to the roundabout. In this work the correctness of the mechanism is mechanically verified with SPIN, a well-known model checker. The verification proceeds as follows: First the mechanism is modeled as a program in Promela, the input language of SPIN. The Promela program is verified against safety and then a liveness property, namely, deadlock freedom. The results show that a certain subtle condition needs to be met to avoid deadlock. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | roundabout / token-based traffic control / model checking / formal verification / deadlock |
| Paper # | ITS2020-43 |
| Date of Issue | 2021-03-08 (ITS) |
| Conference Information | |
| Committee | ITS / IEE-ITS |
|---|---|
| Conference Date | 2021/3/15(1days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | Online |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | Information Processing for ITS, etc. |
| Chair | Tomotaka Wada(Kansai Univ.) / 細野 裕行(日本大学) |
| Vice Chair | Yusuke Takatori(Kanagawa Inst. of Tech.) / Hiroyuki Hatano(Mie Univ.) |
| Secretary | Yusuke Takatori(Univ. of Tokyo) / Hiroyuki Hatano(Akita Prefectural Univ.) / (名古屋電機工業) |
| Assistant | Msataka Imao(Mitsubishi Electric) / Yanlei Gu(Ritsumeikan Univ.) / Kenshi Saho(Toyama Prefectural Univ.) / 滕 琳(日本大学) |
| Paper Information | |
| Registration To | Technical Committee on Intelligent Transport Systems Technology / Technical Meeting on Intelligent Transport Systems |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Model Checking-Based Verification of Token-Based Traffic Control for Roundabouts |
| Sub Title (in English) | |
| Keyword(1) | roundabout |
| Keyword(2) | token-based traffic control |
| Keyword(3) | model checking |
| Keyword(4) | formal verification |
| Keyword(5) | deadlock |
| 1st Author's Name | Tatsuhiro Tsuchiya |
| 1st Author's Affiliation | Osaka University(Osaka Univ.) |
| 2nd Author's Name | Satoshi Otsuka |
| 2nd Author's Affiliation | Hitachi, Ltd.(Hitachi) |
| Date | 2021-03-15 |
| Paper # | ITS2020-43 |
| Volume (vol) | vol.120 |
| Number (no) | ITS-428 |
| Page | pp.pp.41-44(ITS), |
| #Pages | 4 |
| Date of Issue | 2021-03-08 (ITS) |