モデル検査法を用いた鉄道信号システムの連動仕様検証

スポンサーリンク

概要

論文の詳細を見る
鉄道信号システムは、障害や誤動作が重大な事故につながるため、安全性に関して厳しい基準が求められている。特に駅構内の交通は輻輳するため、安全の確保のためには複雑な運行制御が必要となる。駅構内の信号機や転轍器の制御を行う装置は連動装置と呼ばれ、保安機能の実現に関して中心的な役割を果たす。一方、安全性・信頼性の高いシステムを実現するための技術として形式的手法が近年注目されている。本研究では、連動装置の制御仕様の形式的検証を行う方法を提案する。連動装置や駅構内の機器の動作を有限状態機械で、これらの装置の動作が満たすべき性質を時相論理式で記述し、有限状態機械上で時相論理式が成り立つかどうかを、モデル検査法と呼ばれる方法で検証する。
社団法人電子情報通信学会の論文
1999-02-05

著者

関連論文

スポンサーリンク