| 講演名 | 2012-05-24 ATP閉そくシステムの仕様妥当性のモデルベース検証(交通関係を主として) 謝 国, 黒田 智也, 望月 寛, 高橋 聖, 中村 英夫, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 新しい鉄道信号システムであるATP閉そくシステムについて,安全性や信頼性が高いソフトウェアの開発のために,形式手法を用いてシステムの仕様書を分析した.まず,自然言語で書かれた仕様書を形式的仕様へ正しく記述するために,状態遷移図を作成した.そして状態遷移図をもとにシステムをUMLでモデル化し,オブジェクト指向分析を行った.さらに,形式手法であるVDM++によりシステムの仕様を記述し,システムの内部整合性や妥当性を検証した. |
| 抄録(英) | In the development of automatic train protection and block (ATPB) railway signalling system, in order to guarantee the safety and reliability of its software system, formal method is adopted to analyze specification formally. Firstly, in order to improve the accuracy of translating original specification into formal specification, dynamic state translation is extracted to express the internal operation mechanism and state changes for every component, e.g. point, signals, trains. Followed by UML model is created for a comprehensive and object-oriented analysis of ATPB. Thirdly, a rigorous specification of system is established by VDM++ unambiguously without understanding deviation. At last, the specification is validated, such as internal consistency and combinatorial testing to ensure not only the correctness of specification itself, but also the satisfiability for the actual requirement. |
| キーワード(和) | 列車信号システム / ATP閉そく / 形式手法 / 仕様書 |
| キーワード(英) | Railway Signalling System / ATPB / Formal Methods / Specification |
| 資料番号 | SSS2012-4 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SSS |
|---|---|
| 開催期間 | 2012/5/17(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Safety (SSS) |
|---|---|
| 本文の言語 | ENG |
| タイトル（和） | ATP閉そくシステムの仕様妥当性のモデルベース検証(交通関係を主として) |
| サブタイトル（和） | |
| タイトル（英） | Model Based Specification Validation for a Novel Railway Signalling System |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 列車信号システム / Railway Signalling System |
| キーワード(2)（和/英） | ATP閉そく / ATPB |
| キーワード(3)（和/英） | 形式手法 / Formal Methods |
| キーワード(4)（和/英） | 仕様書 / Specification |
| 第 1 著者 氏名（和/英） | 謝 国 / Guo Xie |
| 第 1 著者 所属（和/英） | 日本大学理工学部 College of Science and Technology, Nihon University |
| 第 2 著者 氏名（和/英） | 黒田 智也 / Tomoya Kuroda |
| 第 2 著者 所属（和/英） | 日本大学理工学部 College of Science and Technology, Nihon University |
| 第 3 著者 氏名（和/英） | 望月 寛 / Hiroshi Mochizuki |
| 第 3 著者 所属（和/英） | 日本大学理工学部 College of Science and Technology, Nihon University |
| 第 4 著者 氏名（和/英） | 高橋 聖 / Sei Takahashi |
| 第 4 著者 所属（和/英） | 日本大学理工学部 College of Science and Technology, Nihon University |
| 第 5 著者 氏名（和/英） | 中村 英夫 / Hideo Nakamura |
| 第 5 著者 所属（和/英） | 日本大学理工学部 College of Science and Technology, Nihon University |
| 発表年月日 | 2012-05-24 |
| 資料番号 | SSS2012-4 |
| 巻番号（vol） | vol.112 |
| 号番号（no） | 52 |
| ページ範囲 | pp.- |
| ページ数 | 4 |
| 発行日 | |