毛兆东， 钱俊彦， 蔡 泳

(桂林电子科技大学 计算机与信息安全学院，广西 桂林 541004)

模型检测[1-2]是一种验证有限状态系统的行为是否具备预期属性的自动验证技术，自提出以来在学术界和工业界产生了巨大的影响，并且已被应用到不同的领域。模型检测的一般过程为：首先对待验证的系统建模，再对待验证的系统属性进行描述，通过模型检测算法验证系统是否满足该属性，若满足，则输出true，否则将给出反例说明模型不满足该属性的原因。

随着计算机系统的复杂性日益增加，系统存在许多不确定性的信息。显然，经典的模型检测方法已经难以准确处理带有大量不确定性信息的系统。为此，人们对经典的模型检测方法进行了扩展。例如，为了对具有随机行为的系统进行定量验证，Hansson等[3]提出了概率计算树逻辑(probabilistic computation tree logic，简称PCTL)的模型检测算法，Baier等[1]提出了基于概率测度的概率模型检测算法。为了解决具有不一致性信息系统的验证问题，文献[4-5]基于多值逻辑对模型检测方法进行扩展，提出了多值模型检测算法。为了解决包含可能性测度量化信息系统的验证问题，文献[6-10]提出了基于可能性测度的模型检测算法。为了解决含有模糊量化信息系统的验证问题，潘海玉等[11]提出了模糊计算树逻辑(fuzzy computation tree logic，简称FCTL)的模型检测算法。

模型检测专注于验证系统是否满足系统属性，当系统不满足属性时无法自动修复系统。由此在模型检测的基础上，Buccafurri等[12]提出了模型检测与自动修复相结合的思想，这引起了研究者的广泛关注。……