Model checker for railway signalling communication protocol

As a very important part in the development of the protocol, verifications for a developed protocol specification are complementary techniques that are used to increase the level of confidence in the system functions by their specifications. Using the informal method for specifying the protocol, a little ambiguity may be contained in the protocol. This indwelling ambiguity in control systems can be the cause of accidents, especially for safety-critical systems. To clear the ambiguity contained in the designed protocol, we use the LTS (Labelled Transition System) model to design the standard protocol for railway signalling systems,. Then we verify the safety and liveness properties automatically and formally, through the model checking method. The modal mu-calculus, which is an expressive method of temporal logic, has been applied to the model checking method. In this paper, we verify the safety and liveness properties of the Korean standard protocol for railway signalling systems. To automatically check the safety and liveness properties of the designed protocol, the formal checker is implemented. The developed tools are implemented by the C++ language under Windows XP.