基于广义符号轨迹赋值模型验证的反例的产生

广义符号轨迹赋值(Symbolic Trajectory Evaluation)引入了符号变量和抽象技术,解决了验证中状态爆炸的问题,但是却为寻找反例制造了很多障碍.针对此,提出了一种高效的寻找反例的算法,它应用集合的概念,通过回溯在父子路径之间进行集合的交集,可以高效地解决抽象引起的问题.并对此算法进行改进,解决了符号变量带来的问题.

Counter-example Generation in Generalized Symbolic Trajectory Evaluation

Generalized Symbolic trajectory evaluation is a powerful model checking technique which introduces symbolic quaternary and symbolic variables into symbolic quaternary assignments. But to find Counter-example has obstacles. In this paper, we presented an solution to search Counter-example. It uses set Intersection to backward simulation to generalized Counter-example. And we extended the solution to solve the problems from symbolic variable.