自動列車制御装置における数値計算へのBメソッド適用の検討

• Item type: Journal(1)
• 公開日: 2015-04-15
• タイトル: 自動列車制御装置における数値計算へのBメソッド適用の検討
• タイトル / 言語: en
• タイトル: Study on Application of B-method to the Numerical Calculation of Automatic Train Protection Systems
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: [一般論文] 形式手法，Bメソッド，数値計算，自動列車制御装置，ブレーキ曲線
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 公益財団法人鉄道総合技術研究所
• 著者所属(英): en
• 著者所属(英): Railway Technical Research Institute
• 著者名: 寺田, 夏樹
• 著者名(英): Natsuki, Terada
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 鉄道の運行を支えている信号保安装置には高い安全性が要求される．その中でソフトウェアの比重は以前に比べて大きくなり，ソフトウェアの安全性を保証するための技術の確立がより重要となっている．数値計算のようなプログラムであってもその正当性を保証する仕組みが必要である．仕様の形式記述を通じてその正当性を定理証明や自動検査によって検証するフォーマルメソッドはその解決策の1つと考えられる．本論文では，フォーマルメソッドの1手法で，段階的詳細化と定理証明を通じたコード生成に特徴を持つBメソッドを，ATC（Automatic Train Control，自動列車制御）システムの許容速度の計算に対して適用した事例について述べる．本来ならば平方根などを含む計算が必要である事例であるが，Bメソッドで許容される整数演算の範囲で実用的な精度で値の計算が可能であり，プログラムが余裕距離や勾配などの制約を満たすことの証明を行い，プログラムの高信頼化を図ることが可能であることを示す．一方で，whileループでのループ不変条件の使用や，計算途中の値を含めて32bit整数の範囲で計算を行う実装上の制約から，多数の証明責務が発生する状況を示し，数値計算にBメソッドを適用する際に生じる問題点を明らかにする．そのうえで数値計算へのBメソッドの適用範囲についても議論を行う．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Signalling equipment requires high reliability. It is required to increase the reliability of software part, even if it is for numerical calculation. It is considered that formal methods are effective to solve the problem, in which the specifications are proved and/or checked for its integrity through the formal description. We applied B-Method, one of the formal methods and characterized by code generation with stepwise refinement and theorem proving, to the calculation of allowable speed of trains concerned with automatic train protection systems. We show that B-Method, in which floating point values are not used, is applicable to numerical calculation with practial precision that usually requires square root, and that the code is proved to satisfy the constraints such as margins and gradients, and gains more reliability. On the other hand, a lot of proof obligations are generated at the implementation phase, related to use of while loop with invariants, and restriction of calculation range within 32bit integer including intermediate values. We show the problem when B-method is applied to numerical calculations, and discuss the applicable range of B-Method to numerical calculations.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN00116647
• 書誌情報: 情報処理学会論文誌; 巻 56, 号 4, p. 1278-1291, 発行日 2015-04-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7764