Research On Formal Modeling And Verification Methodology Of TCN System

With the technical development of fieldbus, computer network communication, embedded system and fault diagnosis, the modern train control system has been developed from digital control system to distributed computer system which is based on network control system. Train network control system which is a special real-time distributed control system can interconnect and control all of the equipments with bus technology. As the coming of high-speed times of railway, self design and research, equipment manufacture, operation and maintenance of train communication network (TCN) system has become the focus of research. Recently, with the thoroughly study of TCN system, some important achievement has been acquired, but some problems such as formal modeling of TCN system and verification of consistency according to TCN standards are becoming more and more obvious in the development of TCN system. This dissertation aims to propose application-oriented new schemes to solve the problems.The achievements about modeling and verification of railway system based on formal and simulation methods are surveyed first. The main line to development flow of TCN system, the classification of TCN standards and the technologies about formal modeling, formal verification and simulation are studied. Some problems in this field are concluded.A rounded framework for formal modeling and verification of TCN system is proposed, which can satisfy the design and verification requirements of TCN system based on technologies of formal sematic, mathematical theory, model checking and simulation.According to the characteristics of TCN system, a hierachical methodology for modeling is described based on the extended Petri net. As validation of the methodology, HRTCPN is used in extracting behaviors and properties of system, and network topology and nodes functional model of TCN system are constructed.Definitions of static properties of HRTCPN model about TCN system is described based on TCN standards and characteristics of the system. After that, the checking rules about static properties are illustrated based on mathematical theories such as linear algebra, graph theory, and etc. Moreover, real-time property of TCN system model is studied based on incidence matrix and S-invariables, and real-time analysis methods and optimization methods are proposed.With the purpose of verification about the dynamic properties of TCN system model, formal verification methodologies based on symbolic model checking and timed automation are given. The transformational rules to the two models from HRTCPN are designed by studying the concepts of symbolic model checing and semantic of timed automation. Dynamic properties of TCN system are verified by means of the combination of the two methodologies, which avoid the states explosion problem owning to hierarchical feature of modeling and verification flow. At the same time, the completeness of dynamic properties verification according to IEC61375 standards is improved.Most of the major functions about TCN protocol is implemented by TCN controller, and it's very important for the verification of TCN controller in the implementation level. Based on the advanced verification methodology, VMM verification methodology, module level and system-level functional verification frameworks are constructed, and network topology level functional verification framework is proposed aiming to covering the shortage of inefficiency of traditional methods about simulation of communications in the network. Mechanisms such as coverage-driven stimuli generation, multi-level coverage collection and sub-unit reuse are adopted for improving the efficiency of simulation. Error injection mechanism is designed on the basis of requirement of reliability in TCN standards which is a solution to the problem of verification about abnormal processing module in TCN controllers. Furthermore, TCN controllers are verified by employing a full range of methods. As a result, the coverage rate and number of bugs identified are greatly improved.Finally, the work of the dissertation is concluded.