鉄道信号システムの連動装置の形式的検証向けモデル化と検証環境構築(ソフトウェア基礎, プログラム理論)
スポンサーリンク
概要
- 論文の詳細を見る
鉄道信号システムは, 列車の位置検知と信号機と転てつ器の動作の制御を行って列車運行の安全を図るシステムであり, その安全性に関して厳しい要求がある.中でも連動装置は駅構内の列車の進路制御を行う装置であり, 鉄道信号システムの保安機能の中心的な役割を果たしている.連動装置の行う制御は比較的小規模な駅でも複雑なものになり, その設計・検査には大きなコストがかけられている.本論文は, 鉄道信号システムの連動装置をモデル検査法を用いて検証するためのモデル化について述べる.またこのモデルをもとにした検証環境を構築したので報告する.連動装置の仕様は連動図表と呼ばれる図表で記述される.連動図表を対応するリレー回路の標準結線に基づいて解釈し, 有限状態機械でモデル化した.検証すべき仕様として, 衝突及び脱線の仕様をLTL式で記述し, 比較的小規模な駅に関しては検証可能であることを確認した.大規模な駅の検証に関しては, 駅の設備を分割して検証する方法を提案した.また, 連動図表のモデル化と仕様記述の負担を軽減するため, 連動装置のモデルと衝突・脱線の仕様を自動作成する連動図表検証環境を構築した.
- 社団法人電子情報通信学会の論文
- 2005-12-01
著者
-
高橋 和子
関西学院大学理工学部
-
藤井 英明
三菱電機株式会社伊丹製作所
-
川村 正
三菱電機株式会社人材開発センター
-
土田 勝紀
三菱電機株式会社伊丹製作所
-
高橋 和子
関西学院大学
-
川村 正
三菱電機株式会社 人材開発センター
関連論文
- 知識変更を伴う議論システム
- 鉄道信号システムの連動装置の形式的検証向けモデル化と検証環境構築(ソフトウェア基礎, プログラム理論)
- 車車間通信を用いた車線変更と脇道にともなう交通流の円滑化を図るモデルの提案と実装
- 帰納的アプローチに基づく理想的電子現金方式のモデル化および証明支援系Isabelle/HOLによる安全性の証明
- 電子現金の分割利用可能性の形式化と帰納的証明
- 車車間通信を用いた車線変更と脇道にともなう交通流の円滑化を図るモデルの提案と実装
- Symmetry Reductionを使ったAISの確率付きモデル検査
- 定性空間推論の新しい枠組DLCSとその上での操作
- 矩形領域に基づく定性空間推論の提案と実装
- 凹凸情報と接触パターンに基づく定性空間表現
- 定理証明器による電子現金プロトコルの検証
- 信念改竄によるばれない嘘の生成
- 輻輳問題を考慮したモバイルエージェントによるアドホックネットワークルーティング(モバイル・アドホックネットワーク(1))
- 定性空間表現の二次元平面への埋め込みについて
- 定性空間表現の二次元平面への埋め込みについて
- ボードゲームBAOにおける周期的動作の解析
- ボードゲームBAOにおける周期的動作の解析(数理モデル一般)
- ボードゲームBAOにおける周期的動作の解析
- ボードゲームBAOのCCSによる記述と解析
- 性質の伝播に関する定性空間推論
- モバイルエージェントを用いた動的ネットワークルーチングシステムの拡張
- 2. 広がるすきま : E. M. ForsterのHowards End, "Only connect..."からA Passage to India, "Perhaps!"へ(日本英文学会第73回大会報告)
- 空間に埋め込まれた意味情報の記述
- マルチエージェントの連鎖的交渉を用いたスケジュール作成と調整(スケジューリング,「Webインテリジェンス」及び一般)
- マルチエージェントの連鎖的交渉を用いたスケジュール作成と調整(スケジューリング,「Webインテリジェンス」及び一般)
- 動的議論システムの意味論的考察
- Symmetry Reduction を使ったAISの確率付きモデル検査
- 「情報処理学会論文誌 : プログラミング」の編集について
- ソフトウェアプロジェクトリーダー育成コースによる人材育成とその効果
- 「情報処理学会論文誌 : プログラミング」の編集について
- 矩形同士の埋め込み型重ね合わせについての定性空間推論
- 定理証明器によって証明されたCプログラムのマージャ