Bメソッドによる単線自動閉そく装置の検証

摘要

ソフトウェアの高信頼化手法としてシステムの仕様を数学的論理的体系を持った仕様記述言語で記述して分析を行うフォーマルメソッドが注目されている．本報告では、証明による検証が可能であり仕様からコードが自動的に生成されるという点に着目してBメソッドを使用し、鉄道の単線区間の運転方向を制御する単線自動閉そく装置をモデル化して検証を実施したので報告する．ここでは単にBメソッドを適用するのではなく、記述がより容易なVDM で最初にモデルを記述し、これをB に記述し直す形で検討を行った．この2つを組み合わせる際の考え方についても合わせて報告する．%Formal methods is expected to increase reliability of software. We report application of B-method tornautomatic block system for single line. In B-method, verification with theorem proving is available and codes arerngenerated from the specification. We not only used B-method, but also used VDM, in which it is easier to describernspecification. We also report how to combline VDM and B.