安全苛刻系统自动化测试的形式化语义模型

安全苛刻系统的可信性需求典型而迫切，其可信性评估和验证具有测试依赖性.安全苛刻系统一般是复杂系统，手工测试实际上不可行，发展自动化测试手段是必然趋势.针对安全苛刻系统测试过程自动化中存在的高阶协同、实时和时序性，以Ambient演算、CCS演算、论域理论等为基础，给出测试过程的高阶协同定义，建立一种层次化演算模型，为测试过程提供一种信息化和自动化手段.模型通过对被测产品、测试设备与测试任务的抽象与组织，给出安全苛刻系统测试过程自动化的工作模式.最后，通过扩展标记转换系统定义，给出高阶协同行为的收敛性和正确性的证明，论证了模型的可计算性，验证了安全苛刻系统测试的可自动化.模型已应用于航天器的自动化测试中，并成为航天器测试行为的日常工作规范.

Formal Semantics Model for Automatic Test of Safety Critical Systems

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.