国产欧美精品一区二区,中文字幕专区在线亚洲,国产精品美女网站在线观看,艾秋果冻传媒2021精品,在线免费一区二区,久久久久久青草大香综合精品,日韩美aaa特级毛片,欧美成人精品午夜免费影视

The safety and integrity level of Computer interlocking software in CBTC(communication based train control) system is SIL4, which is high security and high reliability software. The current widely used software testing and simulation results rely heavily on the selected test vector, to ensure high coverage of the test is very difficult. EN50128 strongly recommended SIL4 level of software using formal methods to complete the software requirements specification and software design, therefore, using formal methods to design software is an important way to build high reliability and high security software. This paper summarizes the existing integrated approaches and advantages and disadvantages of the interlocking subsystem in the CBTC system, and uses the ETDFA (event deterministic finite automata) model to realize the formal definition of upgrade type interlocking software, which ensures the correctness of the interlocking logic, and reduces the uncertainty description of the software. This paper takes creating route as an example to generate the ETDFA model of the interlocking object, and verifies the validity and feasibility of the method. This method not only provides new ideas for the design and development of CBTC interlocking software, but also contributes to the formal verification and analysis of security demanding software, and improves the security and correctness of interlocking software.