Model-based test generation techniques verifying the on-board module of a satellite-based train control system model

Testing as a means of verification during system development, aims at demonstrating the compliance of actual and intended behaviours of the system. However, the degree of automatic test generation and test coverage are big challenges in testing. Concerning these problems, two approaches are proposed to test the on-board module of an advanced satellite-based train control system model. The first approach is a model-based test generation technique based on Coloured Petri Nets (CPNs). The test model includes a behavioural module of the on-board subsystem model and two other modules for the application environments of the onboard subsystem model. The behavioural module and modules of application environments form a closed system. The expected output of a test case is extracted from a path of the reachability graph of the test model. Beside the CPN based approach for generating test cases, another model-based test generation technique is applied. This method uses a special Petri net dialect called Safe Place Transition Net with Attributes (SPENAT) to model the intended behaviour of the test object, the on-board subsystem model in this case. No environment of the test object has to be modelled, because of the possible input/output modelling with a SPENAT. Thereby, a SPENAT is an open system and its transitions can be triggered by external events with parameters (external data). The identification of suitable test cases is based on the construction of a (complete) prefix of the SPENAT model and the specified coverage criteria. With CPN based (closed system) and SPENAT based (open system) approaches, the verification of a railway operations control system model, such as the on-board subsystem model in this case, could be done by testing. At last, the results of both approaches are discussed and the advantages as well as disadvantages are illustrated.