The Formal Modelling And Model Checking Research Of Rail Transportation Train Control System

In modern public transportation system, rail transportation plays a vital role. At present, the Chinese rail transportation system has been going through a period of rapid improvement and innovation, and People are looking forword to more and more comfortable and fast transportation facilities. It is a big challenge to ensure the safety and great efficiency of rail transportation which train control system plays an important role. With the rapid development of computer technology, the safety assurance methods and technologies formerly used could no longer satisfy the ever increasing safety demand of complex computer system. Recently, Formal methods which based on discrete mathematics and formal logic theory improve rapidly, and give a possible solution to safety assurance of complex computer system.The dissertation is focusing on the research of formal modeling and model checking of rail transportation train control system. TAN (Timed Automata Network) model is proposed to describe computer system, then the safety and correctness of system design is verified by model checking of TAN. Besides, formal development framework —— ForTAN (Formal Design and Verification Methods based on Timed Automata Network) is proposed and applied to onboard ATP system of Dalian 3rd rapid rail line. These works are significant for development of train control system, improving the safety management, mastering the key technologies in rail transportation and conducting practice and development of rail transportation in China. The main innovative works are:(1) TAN (Timed Automata Network) model is proposed to deal with train control system and the formal definition and characters are given based on finite automata theory. And TAN language is given to describe and record TAN model. The advantages of Timed Automata Network are: ①The complexity of system can be decomposed by TAN, and the problem of states explosion can be solved partly compared to typical Automata theory; ②The time character of system can be described by time constraints between Component Automata; ③The concurrency of the system can be described by the action sets among components automata; ④The defect of typical automata theory that infinite states can not be described is solved by partition methods of continuous variables.