Model Based Safety Testing Method For High-speed Train Control System

During the rapid development of Chinese High-Speed Railway,train control system is adopting advanced information and communication technology.As a result,railway transportation efficiency is vastly improved in China.But new risks have emerged at the same time,which put new challenges with respect to railway safety in front of us.On one hand,train control system needs to perform safety related functions correctly to ensure safety control.On the other hand,train control system needs to ensure that no hazard could happen in case a component had a fault during the operation.It is very important to perform safety testing on train control system in order to verify and validate its safety performance and to unfold any safety defect that exists in it.This thesis is focused on generating test cases to test train control system's safety function and to test its fail-safe performance.To test train control system's safety function,current researches mainly use discreteevent model or real-time model as the reference model in MBT(Model-Based Testing)to generate test case.As those models cannot describe hybrid behavior,it is impossible to verify the safety property of the closed system composed of train control system and train.Also,current researches lack justification of the reference model's adequacy,and test suite optimization method targeting at critical logic.To solve these problems,a safety function test case generation method based on HCSP(Hybrid CSP)is proposed,in which safety function test case is automatically generated by using HCSP as the reference model.To test train control system's fail-safe performance,current researches mainly use an integrated model which contains behavior information in both normal and abnormal condition to generate test case.The model used is discrete-event model,and the information compatibility issue is ignored is model integration.To solve these problems,a fail-safe test case generation method based on HCSP is proposed,in which an integrated HCSP model is model checked to generate input sequence that can lead faulty train control system to hazard.The innovations of the thesis are as follows:1).A reference model construction and verification approach for train control system safety function testing based on HCSP is proposed.The STAMP theory is combined with AG(Assume-Guarantee)Reasoning to solve its components partition problem.The main idea is analyzing coupling relations between components using the STAMP safety control structure.The HCSP reference model is verified by compositional verification approach to justify its correctness.The adequacy of reference model is also justified by the scenario-based analysis process proposed in the thesis.2)A test case generation method to test train control system's safety function based on HCSP reference model is proposed.By defining RHCSP,a subset of HCSP,and RHCSP's operational semantics in STS,the gap between HCSP and I/O-equivalence class partition test method is filled.A complete safety test suite generation approach based on static analysis of safety property is also proposed on the basis of that.By eliminating vacuous and redundant test cases with respect to given safety property,test efficiency can be improved.In our experiment,up to 95% the size of test suite was reduced without affecting test effectiveness,which proves the effectiveness of this approach.3)An input constraint description and solution generation method based on timed automata is proposed.Time automata is used to describe the input constraint and the set of candidate input sequences,an input sequence that fits input constraint is generated by model checking the automata network.This work fills the gap that I/O-equivalence class partition test method cannot deal with complex input constraint.4)A fail-safe test case generation method to test train control system's safety performance after equipment fails based on HCSP is proposed.The integrated HCSP model is generated automatically using an ontology-based approach,which solves the problem of information compatibility.An HCSP-to-TA transformation function is defined to transform HCSP into TA,so model checking can be performed.In our simulation,a fail-safe test case generated using this approach led the train to an accident,while tradition fail-safe test method didn't.It proved the effectiveness of this approach.