| CTCS-3 train control system is a train control system widely used in China at present.It is a crucial control system to guarantee the safe operation of trains,and its safety requirements are becoming more and more severe.Before being put into application,comprehensive and rigorous safety function testing is required.The safety function test of the train control system is carried out by inputting a specific test case set and comparing the output behaviours with the specific expression of the operation scenario.Testing system scenarios under special conditions is more helpful to optimize the completeness and representativeness of train control tests.The temporary speed restriction scenario describes the vehicle control behaviours of the undercarriage control system in a special state,but the working mode is not continuous,and the relevant scheduling commands only take effect within a certain period.The particularity of its scenario requires higher requirement on the generation efficiency and fault coverage of test cases.At present,most of the test case generation methods for temporary speed restriction scenario are based on expert experience and engineering experience,and the efficiency of the generation method and the completeness of the cases can be further improved.Based on this,this thesis deeply combines safety analysis,formal modelling theory and mutation testing theory,and designs a test case generation method for temporary speed restriction scenario based on mutation testing.This work is mainly divided into the following three points:(1)In order to comprehensively analyse the impact of system interaction on overall safety in the temporary speed restriction scenario,this thesis uses the STPA safety analysis method to clarify the system-level dangers of the temporary restriction scenario to people and the environment,and constructs a hierarchical control structure block diagram of the scenario.Combined with the STPA guide words,unsafe control behaviours are distinguished.Appropriate control process model can be selected and control defects with one of the unsafe control behaviours can be detected,and finally scenario safety constraints will be proposed.(2)In order to simplify the scene description,this thesis combines the main controllers in the hierarchical control structure and the interaction between the controllers,uses the timed automata theory and the UPPAAL environment to build the model of each controller,and calculates the construction time of all member models.Automata network model is based on all these,and the dynamic execution of the model to verify the security and liveness of the model can be simulated.Then,the safety constraints are deeply integrated with system modelling and verification,and a timed automaton network model of temporary speed restriction scenario injected with safety constraints is constructed.(3)In order to complete the test case set and improve the fault coverage of the test case,this thesis derives a new test case set based on the known fault set based on the mutation testing technology and the timed automaton model that conforms to the system specification.Firstly,mutation operators that are functional and free from grammatical errors are designed and their formal description in time automata is given.Secondly,inject the mutation operator to generate the variant,and check the consistency with the corresponding model of the original scene,and then use the bounded model checking technique to traverse the observable behaviours included in the longest path of all non-equivalent variants,and generate the original test cases.Finally,the test cases are filtered,divided and collected,and several test cases related to temporary speed restriction scenario are obtained.The test case generation method proposed in this thesis more intuitively describes the system interaction logic and related behaviours,generates reusable models,and improves test efficiency.At the same time,test cases are generated based on small defects not detected by other tests,which further improves the completeness of test cases. |