This paper proposed a mutation model-based test case generation method of the Chinese train control system with automatic train operation function. According to several related system specifications that had been issued, took the typical Temporary Speed Restriction Server (TSRS) handover scenario as an example to build the Symbolic Model Verifier (SMV) model of it. By using Computation Tree Logic (CTL) formula to describe the properties of the model, and the model checker NuSMV to model checking the established SMV model in order to confirm the model is correct. Then, according to the characteristics of the train control system, several mutation operators are being thoughtfully selected, which would apply to the model to mutant and generate many mutation models. Putting these mutation models into NuSMV to check models, NuSMV automatically generated set of counter examples, by extracting counter example paths, test cases were finally generated. The results show that compared with traditional method, the proposed method reduce the task of generate test cases and abundant the test suites.
Mutation Model-Based Test Case Generation of Chinese Train Control System with Automatic Train Operation Function
2018-12-01
214533 byte
Conference paper
Electronic Resource
English
Mutation-Based Test Case Generation of Train-Ground Transmission Function for CTCS
Springer Verlag | 2020
|Mutation-Based Test Case Generation of Train-Ground Transmission Function for CTCS
British Library Conference Proceedings | 2020
|Train operation and automatic train control
Engineering Index Backfile | 1921
|TRAIN GROUP CONTROL DEVICE AND AUTOMATIC TRAIN OPERATION SYSTEM
European Patent Office | 2021
|