Modeling and formal verification of SMT rail interlocking system using PyNuSMV

摘要

The success of urban smart mass transportation (SMT) system lie down in their ability to give frequent, fast, safe, and comfortable journeys in the urban conglomeration. In the railway signaling province, a railway interlocking is a computerized system that manages the railway signaling entities to permit a risk-free operation of the train traffic. Being a safety-critical system, the development of a railway interlocking systems follow several standards, such as CENELEC EN50126, EN50128, and IEC62279, which suggest the use of finite state machine inside the system modeling phase, and formal methods in verification, and validation phases. Often, they do verification and validation of railway interlocking tables physically and is thus fault-prone and expensive. So, within our research work, we used nuXmv as a modeling tool, and PyNuSMV as a verification tool, for verifying safety and liveness properties. As well, the reliability of the developed model has been validated by means of counterexamples and custom CTL model checking algorithm. We can also apply our developed model on real urban railway interlocking systems.