模型检测中虚假反例检测方法

摘要

抽象技术是解决模型检测状态空间爆炸的一种有效方法,但其中一个重大的障碍是对系统的抽象会引入原始系统中本来不存在的行为,即可能会引入虚假反例.因此,需要根据反例对抽象模型进行精化.如何判定一个反例是虚假反例还是真实反例,在抽象精化过程中相当重要.本文根据状态的前驱和后继定义失效状态,给出虚假反例的定义,并基于此提出检测虚假反例的并行算法.%In model checking,abstract technology is an effective method to solve the state space explosion,but one of the major obstacles is the abstraction of original system may incur some behaviors that does not exist in the original system,i.e.may incur false counterexamples.Therefore,abstraction refinement should be done based on counterexample.How to judge a eounterexample is true or false is very important in the process of abstraction refinement.According to the definition of failure state which is based on pre and post state,the definition of the false counterexample is proposed,and then two algorithms of false counterexample detection are given.