Formal Verification of a Railway Interlocking System by the SPIN Model Checker

DOI IR (HANDLE) Web Site Open Access
  • Oogami Shigeyuki
    Department of Intelligent Systems, Graduate School of Information Science and Electrical Engineering, Kyushu University : Master's Program
  • Shimizu Ryo
    Department of Intelligent Systems, Graduate School of Information Science and Electrical Engineering, Kyushu University : Master's Program
  • Koshimura Miyuki
    Department of Intelligent Systems, Faculty of Information Science and Electrical Engineering, Kyushu University
  • Kawamura Tadashi
    Advanced technology research institute, Mitsubishi Electric Corporation
  • Fujita Hiroshi
    Department of Intelligent Systems, Faculty of Information Science and Electrical Engineering, Kyushu University
  • Hasegawa Ryuzo
    Department of Intelligent Systems, Faculty of Information Science and Electrical Engineering, Kyushu University

Bibliographic Information

Other Title
  • 鉄道信号システムのモデル検査器SPINによる検証
  • テツドウ シンゴウ システム ノ モデル ケンサキ SPIN ニ ヨル ケンショウ

Search this article

Description

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.

Journal

Related Projects

See more

Keywords

Details 詳細情報について

Report a problem

Back to top