| 講演名 | 2009-12-11 Bメソッドによる単線自動閉そく装置の検証(安全性及び一般) 寺田 夏樹, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | ソフトウェアの高信頼化手法としてシステムの仕様を数学的論理体系を持った仕様記述言語で記述して分析を行うフォーマルメソッドが注目されている.本報告では、証明による検証が可能であり仕様からコードが自動的に生成されるという点に着目してBメソッドを使用し、鉄道の単線区間の運転方向を制御する単線自動閉そく装置をモデル化して検証を実施したので報告する.ここでは単にBメソッドを適用するのではなく、記述がより容易なVDMで最初にモデルを記述し、これをBに記述し直す形で検討を行った.この2つを組み合わせる際の考え方についても合わせて報告する. |
| 抄録(英) | Formal methods are expected to increase reliability of software. We report application of B-method to automatic block system for single line. In B-method, verification with theorem proving is available and codes are generated from the specification. We not only used B-method, but also used VDM, in which it is easier to describe specification. We also report how to combine VDM and B. |
| キーワード(和) | 鉄道信号 / フォーマルメソッド / Bメソッド / VDM / 単線自動閉そく装置 / 自動証明 |
| キーワード(英) | railway signaling / formal methods / B-method / VDM / automatic block system for single line / theorem proving |
| 資料番号 | DC2009-61 |
| 発行日 |
| 研究会情報 | |
| 研究会 | DC |
|---|---|
| 開催期間 | 2009/12/4(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Dependable Computing (DC) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | Bメソッドによる単線自動閉そく装置の検証(安全性及び一般) |
| サブタイトル（和） | |
| タイトル（英） | Verification of Automatic Block System for Single Line by B-method |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 鉄道信号 / railway signaling |
| キーワード(2)（和/英） | フォーマルメソッド / formal methods |
| キーワード(3)（和/英） | Bメソッド / B-method |
| キーワード(4)（和/英） | VDM / VDM |
| キーワード(5)（和/英） | 単線自動閉そく装置 / automatic block system for single line |
| キーワード(6)（和/英） | 自動証明 / theorem proving |
| 第 1 著者 氏名（和/英） | 寺田 夏樹 / Natsuki TERADA |
| 第 1 著者 所属（和/英） | (財)鉄道総合技術研究所 Railway Technical Research Institute |
| 発表年月日 | 2009-12-11 |
| 資料番号 | DC2009-61 |
| 巻番号（vol） | vol.109 |
| 号番号（no） | 334 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |