The Design And Formal Verification Of ATS System Inner Communication Protocol

In Communication-based Train Control System, Automatic Train Supervision subsystem monitors train lines and provides various aspects of practical running information for scheduling staff. Exchanging data among devices of ATS System are completed through inner communication protocol, communication protocol is just like channels of system, which makes system equipment linked to an organic whole , so that each sub-system modules together to complete the specifical function, good or bad quality of communication protocol is directly related to system's function, performance advantages and disadvantage.Traditional communication protocol mostly verified the correctness of protocol design by a large number of experiment. This method can't prove the correctness of the design of communication protocol at a theoretical point of view, but also very difficult to find some hidden design bugs. Therefore, the verification to design model is very meaningful by formal method. In this paper, we designed and verified the inner communication procotol of researching independently ATS system in our laboratory, at the same time, we analysed the verification result.Firstly, we introduced the formal verification method, the meaning of formal verification method is which can prove the correctness of systematic, because it will traversal all the state space and judge every situationism. Then, paper introduce the principle of symbolic model checking and SMV tool, at the same time, introducing the basic working principle and the basic semantics of grammar of SMV, pointing out some problems which were found in the course of using SMV.Secondly, paper designed inner commucation protocol based on demand. Paper introduce the design toolbar Rational Rose in brief, then article describes needs of the communication protocol ATS system and corresponding design strategy. Secondly, we carried out module partition and module design of ATS System inner communication protocol. Finally, paper describe a summary of design process of module which provide the basis for the latter formal verification.Finally, paper verified inner communication protocol with formal method, by the means of abstracting the infinite state transfer diagram, we use SMV language to describe the model which will be verified and use CTL formula to express the property which will be verified. We improved the model of operating the critical regional, so as to verify successfully finally, the verification single pass for the models of processing critical data message, data redundancy procession, data out-of-order procession. Through the verificating of inner commucation protocol, we prove that the protocol which we designed is correct and ensure the quality of inner communications.