The Formal Research Of The Communication Mechanism Of Train To Ground In CTCS-4

Chinese Train Control System (CTCS) is a complex huge system, which is a specificapplication of distributed intelligent systems. In recent years, the formal modeling andverification of the Multi-Agent Systems (MAS) is one of the cutting-edges, In this paper,MAS theory is applied to the train control system innovatively to ensure the normaloperations of the system and achieve the appropriate safety specifications. In this paper, weabstract the communication of train to ground scenario in the system as MAS to study.Firstly, the concepts and methods of formal modeling were introduced. Then the basicknowledge and concept of communicating sequential processes (CSP) and Multi-AgentSystem (MAS) were introduced, The paper described the CSP’s basic principles, and theprocesses of modeling and validation of the model in its associated model verifier-FDR2platform.Second, this paper combined CSP language and multi-agent theory, modeling andsimulation the problem of train to ground communication interactive process in RBChandover scenario in CTCS-4. The paper described the integrity and security of the protocolin train to ground communication in RBC handover, then simulated and analysis thecommunication protocol when injected the failure into the system.In addition, the paper combined the CSP language and the theory of Intelligent Agent,modeling and simulating among the train to ground communication process in Train ControlSystem. Then simulating the above models in the platform, combined with the characteristicsof CSP language, establish relevant security protocol model and prove that the system issecurity. Then the paper use TIMENET4.0formal modeling and quantitative analysis of theregistered protocol model by injecting faults into the communication process in RBChandover, come up with the viewpoint that increased number of trains and the informationsent cycle have impact on the communication delay. It has the instruction significance toCTCS-4system. Final the paper’s results showed that, the combination of MAS and CSPproposed by the paper has some applicability, the MAS model can be tested for safety and toensure that safety-critical requirements of the system. CSP language has a strong ability todescribe the system, provide a theoretical reference basis for the specification and the projectimplementation of the future design for CTCS-4.Finally, the paper made a relatively comprehensive summary of the research, includingthe conclusions and innovation of this paper, and focus on the next step to make the prospect.