SCADE-Model-based Testing Method Of The Onboard ATP Software

Automatic Train Protection(ATP)is the core of train control system,which is responsible for monitoring train speed and preventing train from speeding.It is a typical safety-critical system.As a safety-critical system,it is very necessary to carry out rigorous test on onboard ATP.The formal method is an important approach to improve the safety and reliability of software systems,especially safety-critical systems.SCADE(Safety Critical Application Development Environment)is a model-based development method,which has been widely used in the field of rail transit signal.At present,the research on SCADE is focused on the model-based development method,and the software testing method based on SCADE is rarely studied.Aiming at the problem that the traditional test methods of onboard ATP software rely on manual compilation and the quality of test cases is difficult to be guaranteed,a test method of onboard ATP software based on SCADE model is proposed.The main contents of this paper are as follows:(1)An onboard ATP function model for testing is built.Based on the data flow diagram and safety state machine in SCADE,the mode transformation model and speed monitoring model of onboard ATP are built.The formal modeling method not only ensures the correctness from model to code,but also ensures the consistency between the model and the system under test.(2)A method of generating state transition paths based on SCADE safety state machine model is proposed.Firstly,the state machine model is transformed into the path migration graph,and then the state transition path is selected from the path migration graph by using the search algorithm according to the all-transitions coverage criterion.The state transition path generated by this method implements all states and all transitions coverage of the safety state machine.(3)A method is proposed to generate test cases from test data obtained from state transition paths.Firstly,the test data satisfying the transition conditions are obtained from the state transition paths according to the modified condition decision coverage criterion and the equivalence class partitioning method.Then,the test cases are obtained by combining the test data set with the state transition paths.Test cases are used to test the onboard ATP model in SCADE environment,and the average coverage rate of the modified condition decision was 80.1%.(4)An automatic test case generation tool is developed.Based on the method proposed in this paper,an automatic test case generation tool is designed and implemented in C#environment.The parsing of SCADE model files and automatic test case generation are realized.The test cases generated can be directly used in SCADE model testing.The research results show that the test case generation method based on SCADE safety state machine model proposed in this paper satisfies the all-transitions coverage and can be directly used in software testing of SCADE development.