A high order collaboration and real time formal model for automatic testing of safety critical systems

The need for safety critical systems (SCS) is both important and urgent, and their evaluation and verification are test-dependent. SCS are usually complex and very large, so manual testing of SCS are infeasible in practice, and developing automatic test approaches for SCS has become an important trend. This paper defines a formal semantics model for automatic test of SCS, called AutTMSCS, which describes behaviors in SCS testing. The model accommodates the high order collaboration in real time and temporariness of SCS testing. Testing tasks, test equipment and products under test are abstracted and architected in three layers, and a method for automatic testing is given. Based on extended label transition system (LTS), the convergency and correctness of the model are proved to demonstrate the computability of the model, indicating that the testing process of SCS can be automatic.