Design And Verification Of Security Communication Protocol In IEEE 802.11 Based CBTC System

Communication based train control(CBTC) system can effectively replenish the deficiency of traditional train control system which is controlled by track circuit. With the features of good safety and high transmission efficiency, CBTC is widely used in city rail traffic system. At present, most CBTC system use IEEE 802.11 based wireless local area network(WLAN) technology which provides an effective support for the information transmission as its data transmission subsystem. This kind of wireless communication subsystem is an open transmission system. Its channel is open, and the information spreads through the radio wave. Therefore this subsystem can easily be interfered by various uncertain factors and attacked by intruders. CBTC system is a safety critical system. The data which transmit in CBTC data communication subsystem are the safety-related data which can ensure the safety of train running. Therefore, an effective safety protection measure is essential to protect the train operation control information.In view of the basic position of security data communication in IEEE 802.11 based CBTC system, European Committee for Electrotechnical Standardization sets the standard EN 50159 specially. Based on this standard and the EURORADIO function interface specification, this thesis designs the CBTC security communication protocol to ensure the safety-related data safe and reliable transmission. During the design process the knowledge of protocol engineering theory is referenced. The design contains protocol services, protocol functions, protocol elements structure, protocol organization, the compilation of protocol text and so on.The protocol described in natural language is not strict, ambiguous and has no uniform description standard. The thesis simulates and describes the CBTC security communication protocol by the formal description language colored petri net(CPN) which has strict syntax and semantics definition and its support tool CPN Tools after the design of protocol. In the modeling process, by using the thought of top-down simple-complex, the top model of CBTC communication protocol is been established. Then the single path protocol model as a basic unit is been established. On this basis, the double path protocol model and the safety protocol model are studied.After established, the protocol model is been verified by using the state space analysis tool. Test results show that the protocol description process has no grammar and semantic error. The established model is fair, bounded, and has no deadlock and livelock phenomena. Accordingly, the design of CBTC security communication protocol is correct. It can be used to guarantee the safe and reliable transmission of information in CBTC system.