信号装置仕様の検証を通じたBメソッドにおける仕様記述法の検討
スポンサーリンク
概要
- 論文の詳細を見る
高信頼性が要求される分野において形式手法を用いることでソフトウェアの信頼性を向上させることが期待されている.我々は鉄道の信号保安制御に関わる装置のうち,単線区間の運転方向を制御する自動閉そく装置について,形式手法の1つであるBメソッドによりモデル化を行い,定理証明による検証を行った.Bメソッドでは検証済みコードの生成が可能であるが,実際にシステム仕様の記述を行うと,記述の正当性を保証するために証明すべき条件である証明責務が大量に生成され,検証作業が困難となる場合が多い.本報告においてもシステムが複雑になるにつれて証明責務の生成数が多くなり,対話的証明の実行数(User Pass)が増えていくことを示す.この結果を受け,本報告では証明責務やUser Passの数と仕様記述の関係を考察し,条件分岐により証明責務の生成数が増えることを示す.また一方で,実行される演算結果が満たすべき条件に,システム変数間の制約として記述される不変条件を含めたり,不変条件の表現に条件分岐の条件を近づけたりすることで,自動証明される証明責務の割合が増え,User Passを減らせることを示す.これに基づき,証明責務やUser Passの数を減らすための仕様記述法を検討した.この手法を単線区間向け閉そく装置の仕様記述に対して適用した結果,証明作業の負担を軽減できたことを報告する.
- 2014-06-10