モデル検査法を用いた鉄道信号システムの連動仕様検証

• Item type: SIG Technical Reports(1)
• 公開日: 1999-02-04
• タイトル: モデル検査法を用いた鉄道信号システムの連動仕様検証
• タイトル / 言語: en
• タイトル: Verification of Railway Interlocking Specifications by a Model Checking Method
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 三菱電機（株）先端技術総合研究所
• 著者所属(英): en
• 著者所属(英): Advanced Technology R&D Center, Mitsubishi Electric Corporation
• 著者名: 川村, 正
• 著者名(英): Tadashi, Kawamura
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 鉄道信号システムは、障害や誤動作が重大な事故につながるため、安全性に関して厳しい基準が求められている。特に駅構内の交通は輻輳するため、安全の確保のためには複雑な運行制御が必要となる。駅構内の信号機や転轍器の制御を行う装置は連動装置と呼ばれ、保安機能の実現に関して中心的な役割を果たす。一方、安全性・信頼性の高いシステムを実現するための技術として形式的手法が近年注目されている。本研究では、連動装置の制御仕様の形式的検証を行う方法を提案する。連動装置や駅構内の機器の動作を有限状態機械で、これらの装置の動作が満たすべき性質を時相論理式で記述し、有限状態機械上で時相論理式が成り立つかどうかを、モデル検査法と呼ばれる方法で検証する。
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: The verification of safety requirements is a fundamental problem in railway signaling system design. Especially, specifications of railway inter-locking systems, which control railway signals and points in a station in a safety-critical manner, become 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 a formal verification method. A railway inter-locking system is described by a finite state machine and safety requirements are described by temporal logic formulas. Then, by a model checking method, the formal verification of the temporal logical specification is done.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11451459
• 書誌情報: 情報処理学会研究報告システムLSI設計技術（SLDM）; 巻 1999, 号 12(1998-SLDM-091), p. 81-88, 発行日 1999-02-04
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会