講演抄録/キーワード |
講演名 |
2008-10-17 15:25
段階的詳細化に基づく鉄道信号へのフォーマルメソッド適用 ○寺田夏樹(鉄道総研) R2008-32 |
抄録 |
(和) |
ソフトウェアの品質向上のための手法としてフォーマルメソッド(formal
methods)が注目されている.これはソフトウェアの仕様をコンピュータに分か
る形で数学的論理的に記述し,それをコンピュータ等の支援による検証を実施す
ることで,仕様の段階で問題点を十分に洗い出し最終的な製品の品質を高めるこ
とを目指している.
大規模なシステムや複雑なシステムに対してフォーマルメソッドを適用する際,
一気に仕様を記述するのではなく,段階的に仕様の記述を詳細にしていく段階的
詳細化手法が有効と考えられる.各詳細化段階での整合性の証明を実施すること
により,仕様を忠実に実行するプログラムを生成することができる.本報告では
信号システムの一例としてATC(自動列車制御装置)のブレーキ曲線の計算プロ
グラムに本手法を適用し,証明と段階的詳細化が有効であることを確認した.ま
た,実際のシステムに適用しやすい段階的詳細化手法についても提案する. |
(英) |
It is expected that formal methods enhance reliability of software.
When the target system is large and complicated, stepwise refinement
seems to be very effective. With this technique, an abstract
specification is written with minimal conditions initially, then it is
refined more precisely until it is ready to be serviceable.
We applied stepwise refinement to calculation of braking curve in
automatic train control system. We report the application and
suggest practical application to other systems. |
キーワード |
(和) |
鉄道信号 / フォーマルメソッド / VDM / 段階的詳細化 / Bメソッド / / / |
(英) |
railway signalling / formal methods / VDM / stepwise refinement / B-method / / / |
文献情報 |
信学技報, vol. 108, no. 243, R2008-32, pp. 27-32, 2008年10月. |
資料番号 |
R2008-32 |
発行日 |
2008-10-10 (R) |
ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
R2008-32 |