System safety property-oriented test sequences generating method based on model checking

In this study, model checking is used to generate a suite of test sequences to validate whether the System Under Test (SUT) satisfies the defined safety properties. Firstly, a Coloured Petri Net (CPN) model is abstracted and derived from the system requirement specification of the SUT with a hierarchical modelling approach. A state space analysis is used to verify the model with respect to a set of correctness criteria that include the absence of deadlocks and livelocks. Secondly, some system safety properties defined by the experts are described with a non-standard query and extended computation tree logic. Finally, based on the model without deadlocks and livelocks, the negation of safety properties could be checked by analyzing the occurrence graph and the strongly connected components graph of the model. If the model does not satisfy the specified property, the process of model checking could return some counterexamples. From these counterexamples, the nodes and directed arcs that include the interface information are picked out as the interface messages, which are used to construct a test sequence. A case study of using this method on a railway control system is presented, where the CPN Tools is used to model and generate test sequences. All reachable states are analyzed to detect violations and generate the safety related test sequences, which include the required data to be executed on the SUT. The result shows this method is time-saving, labour-saving and can guarantee the conformance between the SUT and the safety properties.