段階的詳細化に基づく鉄道信号へのフォーマルメソッド適用

スポンサーリンク

概要

論文の詳細を見る
ソフトウェアの品質向上のための手法としてフォーマルメソッド(formal methods)が注目されている.これはソフトウェアの仕様をコンピュータに分かる形で数学的論理的に記述し,それをコンピュータ等の支援による検証を実施することで,仕様の段階で問題点を十分に洗い出し最終的な製品の品質を高めることを目指している.大規模なシステムや複雑なシステムに対してフォーマルメソッドを適用する際,一気に仕様を記述するのではなく,段階的に仕様の記述を詳細にしていく段階的詳細化手法が有効と考えられる.各詳細化段階での整合性の証明を実施することにより,仕様を忠実に実行するプログラムを生成することができる.本報告では信号システムの一例としてATC(自動列車制御装置)のブレーキ曲線の計算プログラムに本手法を適用し,証明と段階的詳細化が有効であることを確認した.また,実際のシステムに適用しやすい段階的詳細化手法についても提案する.
社団法人電子情報通信学会の論文
2008-10-10

著者

寺田夏樹
(財)鉄道総合技術研究所信号通信技術研究部信号

関連論文

もっと見る

スポンサーリンク