Formal verification of a railway interlocking system by the SPIN model checker

Shigeyuki Oogami, Ryo Shimizu, Miyuki Koshimura, Tadashi Kawamura, Hiroshi Fujita, Ryuzo Hasegawa

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)


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.

Original languageEnglish
Pages (from-to)33-38
Number of pages6
JournalResearch Reports on Information Science and Electrical Engineering of Kyushu University
Issue number1
Publication statusPublished - Mar 2005

All Science Journal Classification (ASJC) codes

  • Computer Science(all)
  • Electrical and Electronic Engineering


Dive into the research topics of 'Formal verification of a railway interlocking system by the SPIN model checker'. Together they form a unique fingerprint.

Cite this