Modeling And Verification Of Level Transition Scene In Train Control System Based On Domain And Timed RAISE

Level transition is one of the main scenes of chinese train control system(CTCS), whether its function can be completed accurately and real time is directly related to train operation efficiency and people,s life and property. With the continuous improvement of automation and intelligent control technology, train control system is in constant change. CTCS-2 and CTCS-3 are two kinds of China,s existing railway line, and how to achieve the level transition under the condition of different line sections is one of the key issues to deal with the current status in the development of train control system. However, the train control system has the characteristics of complicated structure, large scale and strong real-time, and each function module in the system of any design flaws may cause serious consequences, therefore how to realize the system architecture and logic function precisely described has become a hot spot and key research in the development of the system. Compared to the simulation and test methods, formal method with strict mathematical logic can not only realize the rigorous description on the system architecture and characteristics, but also strictly verify the system characteristics, and it has become an important method for modeling and verification of safety critical system in recent years.In the dissertation, domain analysis method and timed rigorous approach to industrial software engineering(Timed RAISE) are used to describe the train control system level transition function module, and implement verification of system information interaction correctness and real-time. The main contents are as follows.Firstly, by analyzing and contrasting the formal modeling research on the level transition function module of domestic and foreign existing train control system, in view of the present situation of Timed RAISE applied to level transition scene is not deep enough, the dissertation deeply analyzes interactive information processing between equipments in level transition scene based on collecting standard specification of system design, and information interaction diagram of level transition scene in fixed point is obtained.Secondly, on the basis of the information interaction diagram, dividing equipment status in the execution of the system, state transition diagram is established; in the condition of summarizing the processing logic of the drivers and responder, the functional status of the scene is obtained.Subsequently, based on the domain model of five tuples, the system architecture of level transition scene is designed and built; through the study of Timed RAISE language specification, according to the formal implementation of domain model characteristic elements, entire formal expression of the level transition scene is achieved.Finally, system design constraints are described as axiom form, and information interaction correctness and real-time are verified according to the Timed RAISE inference rules and formal description of system function module.The dissertation deeply analyzes the information processing logic between system each part in the level transition scene, formes standard formal representation of system scene, provides a basis for system architecture design and develop, can guarantee the semantic consistency and correctness of the module functional description in the system development life cycle, can improve the efficiency of system design and development.