| 摘要: |
| 安全苛刻系统的可信性需求典型而迫切，其可信性评估和验证具有测试依赖性.安全苛刻系统一般是复杂系统，手工测试实际上不可行，发展自动化测试手段是必然趋势.针对安全苛刻系统测试过程自动化中存在的高阶协同、实时和时序性，以Ambient演算、CCS演算、论域理论等为基础，给出测试过程的高阶协同定义，建立一种层次化演算模型，为测试过程提供一种信息化和自动化手段.模型通过对被测产品、测试设备与测试任务的抽象与组织，给出安全苛刻系统测试过程自动化的工作模式.最后，通过扩展标记转换系统定义，给出高阶协同行为的收敛性和正确性的证明，论证了模型的可计算性，验证了安全苛刻系统测试的可自动化.模型已应用于航天器的自动化测试中，并成为航天器测试行为的日常工作规范. |
| 关键词: 安全苛刻系统 测试 自动化测试 设备协同 高阶演算 标记转换系统 实时 |
| DOI：10.13328/j.cnki.jos.004412 |
| 分类号: |
| 基金项目:国家自然科学基金（61300007，61003016）；软件开发环境国家重点实验室开放基金（SKLSDE-2012ZX-28，SKLSDE-2013ZX-11） |
|
| Formal Semantics Model for Automatic Test of Safety Critical Systems |
|
LÜ Jiang-Hua, MA Shi-Long, LI Xian-Jun, GAO Shi-Wei
|
|
State Key Laboratory of Software Development Environment (School of Computer Science and Engineering, BeiHang University), Beijing 100191, China
|
| 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. |
| Key words: safety critical systems (SCS) test automatic test equipment collaboration high order LTS real time |
