Analysis of safety properties for vital system communication protocol

Railway signaling systems is a vital control system which is responsible for preventing the train collision from functions such as speed control and route control between trains. As the recent advances of electronic and telecommunication technologies, the existing signaling system has been replaced with new electronic ones. When it comes to the configuration by micro-processors, the interface link among those computerized signaling systems are relied on telecommunication. As the increasing interface link among computerized signaling systems, the guarantee of safety and accuracy of communication protocol has been important problems. To secure communication protocol accuracy and safety, formal methods are applied to verify the safety characteristics of designed protocol for railway signaling system. And also the analysis approach has been studied for comparison with the requirement of international standard related railway communication safety.