Journal of Software:2014.25(3):489-505

(软件开发环境国家重点实验室北京航空航天大学 计算机学院, 北京 100191)
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)
Chart / table
Similar Articles
Article :Browse 2560   Download 2481
Received:September 13, 2012    Revised:April 09, 2013
> 中文摘要: 安全苛刻系统的可信性需求典型而迫切,其可信性评估和验证具有测试依赖性.安全苛刻系统一般是复杂系统,手工测试实际上不可行,发展自动化测试手段是必然趋势.针对安全苛刻系统测试过程自动化中存在的高阶协同、实时和时序性,以Ambient演算、CCS演算、论域理论等为基础,给出测试过程的高阶协同定义,建立一种层次化演算模型,为测试过程提供一种信息化和自动化手段.模型通过对被测产品、测试设备与测试任务的抽象与组织,给出安全苛刻系统测试过程自动化的工作模式.最后,通过扩展标记转换系统定义,给出高阶协同行为的收敛性和正确性的证明,论证了模型的可计算性,验证了安全苛刻系统测试的可自动化.模型已应用于航天器的自动化测试中,并成为航天器测试行为的日常工作规范.
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.
文章编号:     中图分类号:    文献标志码:
基金项目:国家自然科学基金(61300007,61003016);软件开发环境国家重点实验室开放基金(SKLSDE-2012ZX-28,SKLSDE-2013ZX-11) 国家自然科学基金(61300007,61003016);软件开发环境国家重点实验室开放基金(SKLSDE-2012ZX-28,SKLSDE-2013ZX-11)
Foundation items:
Reference text:


LÜ Jiang-Hua,MA Shi-Long,LI Xian-Jun,GAO Shi-Wei.Formal Semantics Model for Automatic Test of Safety Critical Systems.Journal of Software,2014,25(3):489-505