Simulation of CTCS-3 protocol with temporal logic programming

This paper presents an approach to simulate and verify the CTCS-3 (Chinese Train Control System 3) protocol with a Modeling, Simulation and Verification Language (MSVL) which is an executable subset of Projection Temporal Logic (PTL). First, the syntax and semantics of PTL and MSVL are briefly introduced. Then, CTCS-3 protocol is briefly presented and a simplified CTCS-3 protocol described by an MSVL program is given, and the property to be verified is specified by a Propositional Projection Temporal Logic (PPTL) formula. Finally, the simulation is conducted by means of the interpreter of MSVL. A dynamic graph showing behavior of train is depicted. Based on the graph, we can verify whether or not the protocol satisfies the property.