Abstract:Safety critical systems (SCS) are very typical and crucial in trustworthiness study, and their evaluation and verification are test-dependent. Since SCS are usually complex and dramatically huge, manual test of SCS is unfeasible in practice, which makes automatic test approaches for SCS an important trend. This paper studies the characteristics of high order collaboration, real time and temporaries in SCS testing, and based on the domain theory, ambient and CCS calculus, it defines a formal semantics for automatic test of SCS, called AutTMSCS, which describes behaviors in SCS testing. Testing tasks, test equipments and products under test are abstracted and architected in three layers, and a procedure of automatic testing is provided in the model. Based on extended LTS, the convergency and correctness of the model are proved to demonstrate the computability of the model, which indicates that the testing process of SCS can be automated. The model had been practically applied to automatic test of spacecrafts, and the system developed based on the model had become the working platform of spacecrafts test service in daily usage.