Formal Verification And Implementation Of Train Control Safety Computer Management Mechanism

As the rapid development of regional economic integration in recent years, the movement of persons between urbans increased, the train operation control system which based on the traditional architecture showing its insufficient gradually. In order to meet the demands for people to travel faster and convenient, ensure the safety and efficiency of transportation, and improve the compatibility of the system operation platform at the same time, the research on the next generation of the train control system has been launched. As the carrier of realizing operation and data processing function, the safety computer is always an important part of the research on the train control system. Working as the nerve center of computer security, the management units primarily implement the mechanism in the operation of the safety computer system, to allocate the operation coprocessors and safety input and output units, and also vote on the output results. For the construction of safety computer platform for train control system, the verification and implementation of the operation management mechanism has a very important theoretical and practical significance. Therefore, based on the structure and specific function of safety computer for the next generation train operation control system which has been proposed, the management mechanism has been verified and guiding the design and implementation of the management unit in the safety computer platform in this article.Based on the researches of domestic and international train control system, the functional requirements of the safety computer of the next generation train control system was analyzed, and its internal structure was described in detail in this article. Then the structure of centralized system was improved, and the design scheme of distributed structure for the safety computer of next generation train control system has been proposed. The management mechanism and control principle of the management domain were designed, and then the specific functional requirements and the running process of management unit were put forward.According to its management function, the related properties were described by the CTL operators, the state machine model was established through the description language of SMV. The formal verification of the related properties of the management mechanism was carried out through the selected formal verification tool of NuSMV, and also the verification results were analyzed to proof that the design of the management mechanism is conformed to the design specifications.In terms of hardware design, based on the principle of differential design, the management unit of management domain which based on MCU was mainly designed in this article, According to the specific functional requirements, completed the design of corresponding hardware modules, and the PCB diagram of MCU logic board was drawn. In terms of software testing, the internal state machine of management unit was implemented in software through the programming, and the FPGA logic board was simulated by PC, to realize the data exchange process with the MCU logic board, and the internal condition of the state machine was monitored by the state monitor which has been designed. At the same time, the method of fault injection was used for the test of the state transition function.Through the analysis on the test results, the management unit which has been designed and implemented based on the MCU in this article, has achieved the desired control mechanism, and realized the initial design goals.