ATP閉そくシステムの形式化とシミュレーション

カテゴリ: 研究会(論文単位)

論文No: PHS12003

グループ名: 【E】センサ・マイクロマシン部門 フィジカルセンサ研究会

発行日: 2012/01/25

タイトル(英語): Formalizing and Simulating Automatic Train Protection and Block System

著者名: 黒田 智也(日本大学),謝 国(日本大学),望月 寛(日本大学),高橋 聖(日本大学),中村 英夫(日本大学)

著者名(英語): Kuroda Tomoya(Nihon university),Xie Guo(Nihon university),Mochizuki Hiroshi(Nihon university),Takahashi Sei(Nihon university),Nakamura Hideo(Nihon university)

キーワード: 列車システム|ＡＴＰ閉そく|形式手法|仕様書|Railway System|ATPB|Formal methods|Specification

要約(日本語): ATP閉そくという新たな列車信号システムの仕様書を形式的な手法で分析を行なった。具体的手法について、まず、実際のシステムの要件を分析に基づいて、システムのUMLのクラス図を作成した上に、VDM++を用いてATP閉そくシステムの仕様書を記述した。さらに、厳密な形式的な手法で、仕様書を分析上で、システムのシミュレータがされた。結果は、仕様書の高品質を示し、ランタイムエラーや矛盾などがないこと分かった。

原稿種別: 日本語

PDFファイルサイズ: 3,926 Kバイト