モデル検査を用いたラウンドアバウトにおける交通量制御方式の検証

摘要

本研究では，形式検証手法であるモデル検査を用いて，ラウンドアバウト型の交差点における車両の交通を制御する方法の検証を行った結果について報告する.検証の対象とする方法では，ラウンドアバウトの進入部にゲートを設け，電子トークンを車両と無線通信によってやりとりすることで，交差点を進行する車両の数を調整する.検証には，代表的なモデル検査器であるSPINを利用した.SPINへの入力言語であるPromela言語を用いて，まず交差点内での車両の追い抜きを制限しないモデルを用いて，まず安全性の検証を行った.次に，ラウンドアバウト内での車の追い越しはない制約を導入し，活性，具体的には，デッドロックの検証を行った.この結果から，デッドロックを生じないための条件を明らかにすることができた.