| 講演名 | 2021-03-15 モデル検査を用いたラウンドアバウトにおける交通量制御方式の検証 土屋 達弘(阪大), 大塚 敏史(日立), |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 本研究では，形式検証手法であるモデル検査を用いて，ラウンドアバウト型の交差点における車両の交通を制御する方法の検証を行った結果について報告する．検証の対象とする方法では，ラウンドアバウトの進入部にゲートを設け，電子トークンを車両と無線通信によってやりとりすることで，交差点を進行する車両の数を調整する．検証には，代表的なモデル検査器であるSPINを利用した．SPINへの入力言語であるPromela言語を用いて，まず交差点内での車両の追い抜きを制限しないモデルを用いて，まず安全性の検証を行った．次に，ラウンドアバウト内での車の追い越しはない制約を導入し，活性，具体的には，デッドロックの検証を行った．この結果から，デッドロックを生じないための条件を明らかにすることができた， |
| 抄録(英) | 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. |
| キーワード(和) | ラウンドアバウト / トークン制御 / モデル検査 / 形式検証 / デッドロック |
| キーワード(英) | roundabout / token-based traffic control / model checking / formal verification / deadlock |
| 資料番号 | ITS2020-43 |
| 発行日 | 2021-03-08 (ITS) |
| 研究会情報 | |
| 研究会 | ITS / IEE-ITS |
|---|---|
| 開催期間 | 2021/3/15(から1日開催) |
| 開催地（和） | オンライン開催 |
| 開催地（英） | Online |
| テーマ（和） | ITS情報処理，一般 |
| テーマ（英） | Information Processing for ITS, etc. |
| 委員長氏名（和） | 和田 友孝(関西大) / 細野 裕行(日本大学) |
| 委員長氏名（英） | Tomotaka Wada(Kansai Univ.) / 細野 裕行(日本大学) |
| 副委員長氏名（和） | 高取 祐介(神奈川工科大) / 羽多野 裕之(三重大) |
| 副委員長氏名（英） | Yusuke Takatori(Kanagawa Inst. of Tech.) / Hiroyuki Hatano(Mie Univ.) |
| 幹事氏名（和） | 小野 晋太郎(東大) / 橋浦 康一郎(秋田県立大) / 高橋 聡(名古屋電機工業) |
| 幹事氏名（英） | Shintaro Ono(Univ. of Tokyo) / Kouichiro Hashiura(Akita Prefectural Univ.) / 高橋 聡(名古屋電機工業) |
| 幹事補佐氏名（和） | 今尾 勝崇(三菱電機) / Yanlei Gu(立命館大) / 佐保 賢志(富山県立大) / 滕 琳(日本大学) |
| 幹事補佐氏名（英） | Msataka Imao(Mitsubishi Electric) / Yanlei Gu(Ritsumeikan Univ.) / Kenshi Saho(Toyama Prefectural Univ.) / 滕 琳(日本大学) |
| 講演論文情報詳細 | |
| 申込み研究会 | Technical Committee on Intelligent Transport Systems Technology / Technical Meeting on Intelligent Transport Systems |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | モデル検査を用いたラウンドアバウトにおける交通量制御方式の検証 |
| サブタイトル（和） | |
| タイトル（英） | Model Checking-Based Verification of Token-Based Traffic Control for Roundabouts |
| サブタイトル（和） | |
| キーワード(1)（和/英） | ラウンドアバウト / roundabout |
| キーワード(2)（和/英） | トークン制御 / token-based traffic control |
| キーワード(3)（和/英） | モデル検査 / model checking |
| キーワード(4)（和/英） | 形式検証 / formal verification |
| キーワード(5)（和/英） | デッドロック / deadlock |
| 第 1 著者 氏名（和/英） | 土屋 達弘 / Tatsuhiro Tsuchiya |
| 第 1 著者 所属（和/英） | 大阪大学(略称：阪大) Osaka University(略称：Osaka Univ.) |
| 第 2 著者 氏名（和/英） | 大塚 敏史 / Satoshi Otsuka |
| 第 2 著者 所属（和/英） | 日立製作所(略称：日立) Hitachi, Ltd.(略称：Hitachi) |
| 発表年月日 | 2021-03-15 |
| 資料番号 | ITS2020-43 |
| 巻番号（vol） | vol.120 |
| 号番号（no） | ITS-428 |
| ページ範囲 | pp.41-44(ITS), |
| ページ数 | 4 |
| 発行日 | 2021-03-08 (ITS) |