Research On Formal Modeling And Verification Methods Of Partition Software Of Train Control Safety Computers

With the rapid application and development of communication technology,control technology and computer technology in the railway field,train control systems have been moving towards the direction of integration and modularization.As core components of train control systems,safety computers carry most of their safety functions,which are typical safety critical systems.Modern safety computers are gradually transforming from the traditional electronic machinery intensive pattern to the software intensive pattern.The proportion of software is gradually rising,and the scale is growing more and more large,leading to the concept of modularization.In order to realize the high fault-tolerant ability of safety computers,partition software is adopted so that softwares of different groups can run independently without affecting each other in time and space.As the concurrency and sharing characteristics of partition software,it brings challenges to system safety and reliability.Formal methods are based on the formal(logical)systems and can support the strict modeling and verification of the computer systems.In the process of system design and development,the nature of the system can be analyzed,processed and proved,and thus its credibility can be improved and guaranteed.This thesis expounded the integrated modular development trend of train control safety computers,structure features and management mechanism of partitioning software.It classified the formal researches of train control safety computers' partition software,and summarized three aspects of research focuses,namely safety,real-time schedulability priorities,according to the requirements of safety computer modeling.In order to make qualitative and quantitative analysis of these indicators,this thesis carried out researches from the following aspects:(1)Aiming at the safety problem of parallel program,the concurrent safety control mechanism based on transaction memory was proposed.Then it was formulated by inference abstract machine and reasoning rules with concurrent separation logic.The reliability of the safety mechanism was verified by reasoning with the invariant proof method,and the results proved that the mechanism can protect the correctness of concurrent programs.Then,a double-two-of-two safety computer platform was built to test the concurrent safety by using two concurrent applications to operate the shared memory,and it was verified that the concurrent safety access of shared resources could be achieved in the concurrent safety control mechanism.(2)Aiming at the problem of real-time,stochatic time Petri net based modeling method of non-Markovian parameters was deeply studied,which overcame the limitation that time parameters in the Petri net models of train control systems must obey exponential distribution.Through introducing relevant parameters to the definition of stochastic time Petri net,non-Markovian time parameters were distinguished,including deterministic distribution,hyperexponential distribution.Then,transient analysis method based on stochatic state class was proposed by building stochatic state tree and calculating Markovian regeneration points,and realizing the analysis of models containing general distribution time parameters.After that,a stochastic time Petri net model of partition communication was established.The proposed algorithm was used for real-time analysis and verification.And the time delay of process data,message data and monitoring data with different scheduling algorithms were analyzed.Afterwards,the real-time performance of partition communication was tested by using a double-two-of-two safety computer platform and open source real-time Ethernet technology of POWERLINK.(3)Aiming at the problem of schedulability,this thesis also expanded the traditional time Petri net and proposed a modeling method with priority time Petri net.Aiming at Time Division Multiplexing global scheduling and preemptive Fixed Priority local scheduling strategies,the problems of non-deterministic execution time and local resource sharing were overcome,and the hierarchical scheduling of real-time applications,including periodic,contingency and jitter tasks,were modeled.Moreover,an analysis algorithm based on state space enumeration was proposed to identify all the paths from task release to task end.It extracted the optimal completion time and the worst completion time,thus verifying whether the task deadline was met and realizing the schedulability analysis of the model.Then,the partition scheduling time information was tested on the double-two-of-two safety computer platform and partition scheduling was realized with the root task scheduling of Vxworks.Finally,on the basis of a summary of the whole work and innovation points,areas to be improved and problems to be further studied were raised.