| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2021-03-15 15:05 モデル検査を用いたラウンドアバウトにおける交通量制御方式の検証 ○土屋達弘（阪大）・大塚敏史（日立）  ITS2020-43 |
|
| 抄録 | （和） | 本研究では，形式検証手法であるモデル検査を用いて，ラウンドアバウト型の交差点における車両の交通を制御する方法の検証を行った結果について報告する．検証の対象とする方法では，ラウンドアバウトの進入部にゲートを設け，電子トークンを車両と無線通信によってやりとりすることで，交差点を進行する車両の数を調整する．検証には，代表的なモデル検査器である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 / / / | |
| 文献情報 | 信学技報, vol. 120, no. 428, ITS2020-43, pp. 41-44, 2021年3月. | |
| 資料番号 | ITS2020-43 | |
| 発行日 | 2021-03-08 (ITS) | |
| ISSN | Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | ITS2020-43 |
|
| 研究会情報 | |
| 研究会 | ITS IEE-ITS |
| 開催期間 | 2021-03-15 - 2021-03-15 |
| 開催地（和） | オンライン開催 |
| 開催地（英） | Online |
| テーマ（和） | ITS情報処理，一般 |
| テーマ（英） | Information Processing for ITS, etc. |
| 講演論文情報の詳細 | |
| 申込み研究会 | ITS |
| 会議コード | 2021-03-ITS-ITS |
| 本文の言語 | 日本語 |
| タイトル（和） | モデル検査を用いたラウンドアバウトにおける交通量制御方式の検証 |
| サブタイトル（和） | |
| タイトル（英） | 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 |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 土屋 達弘 / Tatsuhiro Tsuchiya / ツチヤ タツヒロ |
| 第1著者 所属（和/英） | 大阪大学 (略称： 阪大) Osaka University (略称： Osaka Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 大塚 敏史 / Satoshi Otsuka / オオツカ サトシ |
| 第2著者 所属（和/英） | 日立製作所 (略称： 日立) Hitachi, Ltd. (略称： Hitachi) |
| 講演者 | 第1著者 |
| 発表日時 | 2021-03-15 15:05:00 |
| 発表時間 | 25分 |
| 申込先研究会 | ITS |
| 資料番号 | ITS2020-43 |
| 巻番号（vol） | vol.120 |
| 号番号（no） | no.428 |
| ページ範囲 | pp.41-44 |
| ページ数 | 4 |
| 発行日 | 2021-03-08 (ITS) |
[研究会発表申込システムのトップページに戻る]