一种抽象模型虚假路径检测的方法

摘要

本发明公开了一种抽象模型中虚假路径的高效检测方法，所述方法具体是，在反例路径中，每个状态是不是失败状态，只与它的前驱状态和后继状态有关。所以，判断时，采用并发执行，通过集合In和集合Out的交集来判断状态是否为失败状态。本发明在检测无穷反例路径时，采用有限前缀分析的多项式比已有的算法短。同时，采用并发技术，能更快的找出失败状态；而且，本发明能更早找到隐藏在反例路径中的失败状态，实验结果显示，系统的规模越大，本发明提出的方法执行的效果越好。