Author(s)

J.-G. Hwang, H.-J. Jo & J. H. Lee

Abstract

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 µ-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. 1 Introductions A few years ago, most of the equipment consisted of vital relay-based systems ensure the safety of railway signalling systems. However, according to the computerization of railway signalling systems, lots of information is exchanged among the computerized railway signalling equipment. By the systemization of railway signalling systems, the communication link is considered more significant than before. Therefore, the communication protocol has to be clearly

Keywords