Designing And Formal Analysis Communication Protocol Of CBTC System

In the Communications-based Train Control (CBTC) system, the reliable data communication between every sub-system is the foundation of the whole system's safety. In order to transfer information safely, a self-contained communication protocol of CBTC system was designed and implemented in this paper, and formalization method was brought in to analyze the protocol in order to prove it s safety performance.In the paper, the design principles of the communication protocol of the CBTC system were expatiated. Firstly, safety requirements and capability targets of the protocol were analyzed according to the demands of the CBTC system at the aspect of safe information transferring; then the safety related communication standard was introduced, and the protocol of the CBTC system was designed hierarchically using the safety defences provided in the standard.In the paper, formalization language CPN, and CPN Tools were chosen to build the models of the protocol from top to bottom. Firstly, the top model of the protocol of the CBTC system was built; then the modeling process of single link protocol was seriously studied. Starting with the basal model, the consummate model of the protocol was obtained by adding each safety defence step by step.The protocol of the CBTC system was validated and analyzed based on the built models by CPN Tools. According to the analysis methods of safety communication protocol, the built models were essentially broken down and predigested firstly, the dynamic characteristics of the models were validated by using the states spaces analysis; then considering different hazards effected the system safety, the capability of the protocol was analyzed, and the average values of different parameters were obtained. Finally, after comparing the averages with the fixed capability targets, the conclusion that the designed communication protocol satisfied the information transferring demands of the CBTC system was educed.