基于有界模型检测的门级软件自测试方法  

Gate-level Software-based Self-testing Method Based on Bounded Model Checking

作　　者：张颖[1] 张嘉琦 王真 江建慧[1] ZHANG Ying;ZHANG Jiaqi;WANG Zhen;JIANG Jianhui(School of Software Engineering,Tongji University,Shanghai 201804,China;School of Computer Science and Technology,Shanghai University of Electric Power,Shanghai 200090,China)

机构地区：[1]同济大学软件学院,上海201804 [2]上海电力学院计算机科学与技术学院,上海200090

出　　处：《同济大学学报（自然科学版）》2018年第11期1575-1581,共7页Journal of Tongji University:Natural Science

基　　金：国家自然科学基金(61432017;61404092)

摘　　要：提出了基于有界模型检测的门级软件自测试方法.将处理器中的模块简化成约束模块,缓解状态爆炸问题.将难测故障的触发条件逐个转化成性质并且采用有界模型检测技术,搜索触发这些性质的违例.最后,将违例映射成测试指令序列,并为测试指令序列添加观测指令序列,构成自测试程序.实验结果表明:该方法在不引起状态爆炸问题的情况下,有效地测试控制器中难以测试的故障,提高了在线测试的测试质量.A gate-level software-based self-testing method based on bounded model checking is proposed in this paper.The module in processor is abstracted and simplified into a constrained module to alleviate the state explosion problem.Then,the trigger conditions for unpredictable faults are transformed into properties one by one,and the bounded model checking is used to search violations which trigger these properties.Finally,the violation is mapped into the sequence of test instructions,and a sequence of observation instructions is added to form a self-test program.The experimental results show that the method can effectively test the faults which are difficult to be tested in the controller but without causing the state explosion problem,and improve the test quality of online test.

关 键 词：基于软件的自测试(SBST) 模型检测 抽象 

分 类 号：TP302.8[自动化与计算机技术—计算机系统结构]