OTS/CafeOBJ 法によるLim-Jeong-Park-Lee 交差点制御プロトコルのモデル化

摘要

本研究ではLim-Jeong-Park-Lee 交差点制御プロトコルにより効率的に走行する片側二車線の交差点をOTS/CafeOBJ法により形式的に記述し，シミュレーションを行い意図した通りの結果を得ることができた．しかし，シミュレーションで良い結果が出たからといって仕様の正しさを証明できたことにはならない．台数を限定し，指示した通りの動きをした場合に限り正しいというだけで，任意の台数について検証していないからである．今後の課題はこの仕様をもとに任意の台数において衝突しないことを検証する．