信号装置仕様の検証を通じたBメソッドにおける仕様記述法の検討

• Item type: Trans(1)
• 公開日: 2014-06-10
• タイトル: 信号装置仕様の検証を通じたBメソッドにおける仕様記述法の検討
• タイトル / 言語: en
• タイトル: Study on Expression of Specification in B through the Verification of Railway Signalling Systems
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: [通常論文] 形式手法，自動閉そく装置，Bメソッド，証明責務，User Pass（優秀論文賞受賞）
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 公益財団法人鉄道総合技術研究所
• 著者所属(英): en
• 著者所属(英): Railway Technical Research Institute
• 著者名: 寺田, 夏樹
• 著者名(英): Natsuki, Terada
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 高信頼性が要求される分野において形式手法を用いることでソフトウェアの信頼性を向上させることが期待されている．我々は鉄道の信号保安制御に関わる装置のうち，単線区間の運転方向を制御する自動閉そく装置について，形式手法の1つであるBメソッドによりモデル化を行い，定理証明による検証を行った．Bメソッドでは検証済みコードの生成が可能であるが，実際にシステム仕様の記述を行うと，記述の正当性を保証するために証明すべき条件である証明責務が大量に生成され，検証作業が困難となる場合が多い．本報告においてもシステムが複雑になるにつれて証明責務の生成数が多くなり，対話的証明の実行数（User Pass）が増えていくことを示す．この結果を受け，本報告では証明責務やUser Passの数と仕様記述の関係を考察し，条件分岐により証明責務の生成数が増えることを示す．また一方で，実行される演算結果が満たすべき条件に，システム変数間の制約として記述される不変条件を含めたり，不変条件の表現に条件分岐の条件を近づけたりすることで，自動証明される証明責務の割合が増え，User Passを減らせることを示す．これに基づき，証明責務やUser Passの数を減らすための仕様記述法を検討した．この手法を単線区間向け閉そく装置の仕様記述に対して適用した結果，証明作業の負担を軽減できたことを報告する．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Formal methods are expected to increase reliability of software, including that of railway signalling systems. We modeled the specifications of automatic block systems for single lines with B, which is one of the formal methods, and verified the model with theorem proving. Although we can obtain verified code with B, more proof obligations are generated to assure correctness of the specification as the specification becomes complicated, which makes the verification difficult. We show that the numbers of proof obligations and user passes to prove them increase as the system becomes complicated. Then we studied the relationships between the expression of the specifcations and the numbers of proof obligations and user passes. We show that use of conditional branch increases proof obligations, while it reduces the number of user passes to approximate the conditions satisfied by operations results to the invariant which is the conditions among system variables. In consideration of the relationships, we have studied how to improve specifications to reduce the number of proof obligations and user passes. We applied the method to the specification of automatic block systems for single line, and reduced the verification process.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 7, 号 2, p. 20-35, 発行日 2014-06-10
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会