Fault Related Formal Test Method Of The Software In Train Control System

ABSTRACT:The software, in the train control system is responsible to implement the key function together with the hardware, thus playing an important part in ensuring the high efficiency and safety of the train operation. The software fault is an important factor in causing an accident, which might cause the social life and property lose. So the research of the software internal fault and external fault tolerance oriented test sequence generating method is significant. The software in train control system has the features of concurrency, reactive and vast behavior space. The research of system-test level black box safety test theory for the software in the train control system should focus on the software exception behavior description oriented modeling method, and the fault related formal test sequence generation method.A dedicated formal modeling method and a test sequence generation method are proposed according to the features and the fault related test requirements of the software in train control system.To the modeling method, a formal definition of the process model and its graphical describing method named Process Describe Method based on Colored Petri Net (ProcCPN) is proposed, a hierarchy modeling method for describing the model of the asynchronous communication based exception behaviors of the concurrent software is then carried out. The characteristics of this method include:(1) It is based on the strict formal definition.(2) It includes hierarchy modeling method, which makes the structure of large-scale software system models clearer.(3) It can describe the communication parameters between processes in an abstract way, and solve the problem of constraint correlation of parameters.(4) It inherited the CPN's merit of graphical description. The System Under Test (SUT) and system weak interoperability based deadlocks statically avoiding method is proposed. It is proved that the satisfaction of weak interoperability is a necessary condition to avoid deadlocks, and not a sufficient condition. The deadlock and livelock analyzing method for software system model is proposed using the Occurrence Graph (OG), the Strongly Connected Component Graph (SCCG), the dead markings and the strongly connected component of the state space. This method can ensure the accuracy of the model and the generated test sequence.To the test sequence generating method, the method of getting the IOLTS semantics of the SUT from the OG of the software is presented. Then the IOLTS semantics based test sequence generation method can be applied directly on the OG given by the CPN Tools. The problem of an excessive number of unreachable states is solved. ASK-CTL is an extension of the Computation Tree Logic (CTL). The definition of witness path for Fault Related Test Purpose (FRTP) formula is proposed based on the ASK-CTL oriented definition of the counterexamples, the witnesses, the formula of FRTP and the evident graph of the FRTP formula. Then the traditional testing theory which uses the counterexamples is extended. The Fault Related Reveal Relation (FRRR) is defined based on the formal definition of Fault Related Observation Objective (FROO) and the extension of the traditional definition of the reveal relation. Then the formal definition of the Fault Related Test Sequence (FRTS) suite is carried out and also proved to be sound and e complete. It promotes the standardization of test sequence generation process. The generation algorithms of the witness paths for FRTP formula, the FROO and the FRTS are proposed and integrated into the CPN Tools. Then the automatic FRTS generation formal method is realized.The presented software system modeling, test sequence generating and test execution methods are applied on the on-board equipment software of China Train Control System Level3(CTCS-3). The results show that these methods can describe the asynchronous communication based exception behaviors of concurrent software and avoid the rapid increase of state space. The generated test sequences for the testing of software faults can test out nearly100%faults in system software. Given a fault tolerance behavior in exception situation, these methods can also generate an exception environment test sequence of Software Fault Injection Test (SFIT) for this behavior.