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.
|Number of pages||6|
|Journal||Research Reports on Information Science and Electrical Engineering of Kyushu University|
|Publication status||Published - Mar 2005|
All Science Journal Classification (ASJC) codes
- Electrical and Electronic Engineering
- Hardware and Architecture
- Engineering (miscellaneous)