Event-Bによる列車監視システムのモニタリング要件の検証

スポンサーリンク

概要

論文の詳細を見る
本稿では,列車監視システムの仕様を形式手法Event-Bによって検証したケーススタディについて報告する.列車監視システムとは,信号機などの設備の状態データを受信し,それら状態データに基づいて列車運行状況をモニタ表示するシステムである.本ケーススタディでは,与えられた仕様に基づいてEvent-Bモデルを作成し,仕様が活性に関する性質を満たすことと,与えられた仕様に矛盾のないことを検証した.Event-Bモデルを使った活性検証のためには,バリアントなど,特定の条件を満たす論理式を発見的に作成する必要がある.本稿では,対象の列車監視システムにおいて上記論理式を作成する方法を提案する.また仕様の矛盾検証では,リファイメントに基づく従来の手段では検証不可能な,外延的かつ部分的に与えられた仕様と内包的に与えらえた仕様との間の矛盾検証方法を提案する.これらの提案方法は,本稿で対象とした列車監視システムに限らず,任意のシステムに対して応用が見込める.
2013-06-15

著者

関連論文

スポンサーリンク