鉄道信号システムのモデル検査器SPINによる検証

DOI 機関リポジトリ (HANDLE) Web Site オープンアクセス
  • 大神 茂之
    九州大学大学院システム情報科学府知能システム学専攻 : 修士課程
  • 清水 亮
    九州大学大学院システム情報科学府知能システム学専攻 : 修士課程
  • 越村 三幸
    九州大学大学院システム情報科学研究院知能システム学部門
  • 川村 正
    三菱電機(株)先端技術総合研究所
  • 藤田 博
    九州大学大学院システム情報科学研究院知能システム学部門
  • 長谷川 隆三
    九州大学大学院システム情報科学研究院知能システム学部門

書誌事項

タイトル別名
  • Formal Verification of a Railway Interlocking System by the SPIN Model Checker
  • テツドウ シンゴウ システム ノ モデル ケンサキ SPIN ニ ヨル ケンショウ

この論文をさがす

説明

The verification of safety requirements is a fundamental problem in railway signalling system design. Especially, specification of railway inter-locking systems, which control railway signals and points in a station in a safety-critical manner, becomes very complex and hard to verify. Recently in this fields, formal verification is expected to be a promising technique for verifying safety requirements. This paper describes how to verify a railway inter-locking specifications by the model checker SPIN which is a formal verification tool. In this method, a railway inter-locking system is described as a finite state machine and safety requirements are given by temporal logic formulas. Then, SPIN checks that the state machine satisfies the requirements.

収録刊行物

関連プロジェクト

もっと見る

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ