モデル検査法による単線自動閉そく装置の検証

摘要

ソフトウェアの高信頼化手法としてシステムの仕様を数学的論理的体系を持った仕様記述言語で記述して分析を行うフォーマルメソッドが注目されている．以前証明による検証が可能なBメソッドを使用して、鉄道の単線区間の運転方向を制御する単線自動閉そく装置の検証を実施したが、近年適用事例が増えているモデル検査法による検証を実施したので、報告する。また、モデル検査法による検証とBメソッドによる証明による検証との比較を行い、その適用範囲を検討した。%Formal methods is expected to increase reliability of software. We reported application of B-method to automatic block system for single line. As an different approach from theorem proving, we applied model checking to automatic block system. We described the precise of the verification, then we compare the two different methods.