符号模型检测反例的研究

摘要

计算机的使用越来越普及，人们对计算机的依赖程度也越来越高。计算机软硬件系统规模也随之日益复杂，如何保证其正确性和可靠性，逐渐成为当前理论界和产业界共同关心的重要问题。因此，形式化方法中的模型检测以其高效、自动化的优点使其在越来越多的领域中被运用。与其他形式化验证方法相比，模型检测的特点在于：第一，模型检测是基于模型而不是基于演绎推理的；第二，模型检测方法不需要激励码，能够自动完成验证工作；第三，模型检测是属性验证过程，当系统模型不满足属性时，模型检测方法能够给出反例，以说明其原因。反例为诊断和修复系统模型的错误提供了依据。从测试的角度，模型检测自动生成反例，可以用于实现测试用例自动化生成。
　　 然而，由于复杂系统的反例通常很长而且难以理解，需要花费很长的时间检查大量的变量和事件，才能够找到错误的真正原因。这就影响了模型检测的效率。在反例构造测试用例时，一个反例可能对应多个属性的违背。因此，产生的测试集往往存在大量冗余的和不必要的测试用例，从而降低了测试执行的效率。
　　 针对上述问题，本文主要的工作及创新点在于：
　　 1、传统的算法是通过穷尽的搜索来找到反例，通过分析传统的算法，本文提出一种改进的算法，该算法将反例中的状态扩展为一个状态集，使用ZBDD来存储所求出的状态集。删除了系统中无关的变量，保留相关的变量。实验分析的结果表明了算法的有效性。
　　 2、由于冗余测试用例的存在会增加测试的成本，现有的化简方法或在测试集产生后在进行化简，或改变和扩展模型检测器使新属性的检测在已进行过的检测基础上进行。因此，本文将研究对模型检测自动化生成的测试用例进行化简，在测试序列产生的过程中进行化简，以剔除原始测试集中可能存在的冗余。