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

提出了基于有界模型检测的门级软件自测试方法.将处理器中的模块简化成约束模块，缓解状态爆炸问题.将难测故障的触发条件逐个转化成性质并且采用有界模型检测技术，搜索触发这些性质的违例.最后，将违例映射成测试指令序列，并为测试指令序列添加观测指令序列，构成自测试程序.实验结果表明：该方法在不引起状态爆炸问题的情况下，有效地测试控制器中难以测试的故障，提高了在线测试的测试质量.
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