Modeling and Verification of TSSM-Based CBTC Zone Controller for Urban Rail Transit

As a safe state machine lacks time property, a TSSM (timed safe state machine) modeling method was presented based on the synchronous design method of reactive system. The weak transition and synchronized transition were defined, and the ZC (zone controller) system model for urban rail transit was established. First, the operation environment, principle and functional requirements of ZC were analyzed, and according to the ZC features of reactive systems, the train management, ZC control, MA calculation and queue management sub-models of ZC system were built using TSSM in SCADE (safety critical application development environment). Then through the TSSM network model of ZC, the interaction information between the sub-models was analyzed. Finally, the safety features of ZC are formally expressed in Lustre, and the functional and performance requirements are examined by running data flow in Design Verifier. The result demonstrates the validity of the bounded liveness and safety properties of the TSSM model, which shows that ZC completely satisfies the functional and safety requirements.