The test of train control system based on Colored Petri Net

Train control systems are important to ensure the high efficiency and safety of train, and the test of it is the key factor which determines whether the system is successful or not. The model checkers of Cad SMV, NuSMV, NuBMC and SPIN have been used to generate test sequence, but the high abstracted model of these tools can not keep all the detail informations to construct the test sequence. Colored Petri Net (CPN) models can reserve all the key details used to generate the test sequence directly. To the best of our knowledge, CPN have not been used in this area, one main reason is that the latest version of the CPN model checking tool can only determine the correctness of temporal logic formulas, and not counterexample is available. In this study, how to generate test sequence for train control system using CPN Tools is introduced. The environment models were used to close the model by the means of reading its script file and getting the input messages set of System Under Test (SUT). Radio Block Center (RBC) is chosen as the SUT and the scenario of Start of Mission is chosen as the example scenario. The result shows that the state space size is related with the environment script files when the SUT CPN model is fixed.