文献

J-GLOBAL ID：201102273642699799   整理番号：11A0174438

モデル検査法による単線自動閉そく装置の検証

Verification of Automatic Block System for Single Line by Model Checking

著者 (1件)： 寺田夏樹 (鉄道総合技術研)
資料名： 電子情報通信学会技術研究報告  (IEICE Technical Report (Institute of Electronics, Information and Communication Engineers))
巻： 110  号： 333(DC2010 51-58)  ページ： 31-35  発行年： 2010年12月03日 
JST資料番号： S0532B  ISSN： 0913-5685  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： ソフトウェアの高信頼化手法としてシステムの仕様を数学的論理的体系を持った仕様記述言語で記述して分析を行うフォーマルメソッドが注目されている。以前証明による検証が可能なBメソッドを使用して,鉄道の単線区間の運転方向を制御する単線自動閉そく装置の検証を実施したが,近年適用事例が増えているモデル検査法による検証を実施したので,報告する。また,モデル検査法による検証とBメソッドによる証明による検証との比較を行い,その適用範囲を検討した。(著者抄録)

シソーラス用語： *モデル検査 ,  *鉄道信号 ,  鉄道信号装置 ,  連動装置 ,  *形式的手法【計算機】 ,  *閉塞装置 ,  鉄道保安装置
準シソーラス用語： SPIN ,  単線自動閉そく装置

分類 (1件)： 信号,保安  (TC01040Y)

引用文献 (12件)：

• ABRIAL, J-R. The B-Book : Assigning programs to meanings. 1998
• 寺田. 段階的詳細化に基づくシステムの高信頼化技法. 信学技報. 2005, 97, 98
• 寺田. Bメソッドによる単線自動閉そく装置の検証. 信学技報. 2009, 109, 334
• POTTER, B. An Introduction to Formal Specification and Z. 1991
• FITZGERALD, J. Modelling Systems-Practical Tools and Techniques in Software Development. 1998

タイトルに関連する用語 (3件)： モデル検査 ,  閉そく装置 ,  検証