Verification and conformance test generation of communication protocol for railway signaling systems

Verification and testing are complementary techniques that are used to increase the level of confidence in the correct functioning of communication systems as prescribed by their specifications. This paper presents an experience of model checking for Korean railway signaling protocol specified in LTS (Labeled Transition System). This formal approach checks deadlock, livelock and reachability for the state and action to verify whether properties expressed in modal logic are true on specifications. We also propose a formal method for semi-automated test case generation for Korean railway signaling protocol described in I/O FSM (Input/Output Finite State Machine). This enables the generation of more complete and consistent test sequence for conformance testing. The above functions are implemented by C++ language and included within RSPVTE (Railway Signaling Protocol Verification and Testing Environment) in the MS-windows environment.