| 講演名 | 2010-12-10 モデル検査法による単線自動閉そく装置の検証(安全性及び一般) 寺田 夏樹, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | ソフトウェアの高信頼化手法としてシステムの仕様を数学的論理的体系を持った仕様記述言語で記述して分析を行うフォーマルメソッドが注目されている。以前証明による検証が可能なBメソッドを使用して、鉄道の単線区間の運転方向を制御する単線自動閉そく装置の検証を実施したが、近年適用事例が増えているモデル検査法による検証を実施したので、報告する。また、モデル検査法による検証とBメソッドによる証明による検証との比較を行い、その適用範囲を検討した。 |
| 抄録(英) | Formal methods is expected to increase reliablity of software. We reported application of B-method to automatic block system for single line. As an different approach from theorem proving, we applied model checking to automatic block system. We described the precise of the verification, then we compare the two different methods. |
| キーワード(和) | 鉄道信号 / フォーマルメソッド / モデル検査法 / SPIN / 単線自動閉そく装置 / Bメソッド |
| キーワード(英) | railway signalling / formal methods / model checking / SPIN / automatic block system for single line / B-method |
| 資料番号 | DC2010-57 |
| 発行日 |
| 研究会情報 | |
| 研究会 | DC |
|---|---|
| 開催期間 | 2010/12/3(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Dependable Computing (DC) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | モデル検査法による単線自動閉そく装置の検証(安全性及び一般) |
| サブタイトル（和） | |
| タイトル（英） | Verification of Automatic Block System for Single Line by Model Checking |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 鉄道信号 / railway signalling |
| キーワード(2)（和/英） | フォーマルメソッド / formal methods |
| キーワード(3)（和/英） | モデル検査法 / model checking |
| キーワード(4)（和/英） | SPIN / SPIN |
| キーワード(5)（和/英） | 単線自動閉そく装置 / automatic block system for single line |
| キーワード(6)（和/英） | Bメソッド / B-method |
| 第 1 著者 氏名（和/英） | 寺田 夏樹 / Natsuki TERADA |
| 第 1 著者 所属（和/英） | (財)鉄道総合技術研究所 Railway Technical Research Institute |
| 発表年月日 | 2010-12-10 |
| 資料番号 | DC2010-57 |
| 巻番号（vol） | vol.110 |
| 号番号（no） | 333 |
| ページ範囲 | pp.- |
| ページ数 | 5 |
| 発行日 | |