无穷状态系统验证中的泛化策略

我们提出一种用于无穷状态系统时序性质自动验证的方法。该验证方法基于约束逻辑程序(CLP)的特化,分两个阶段进行:(1)第一阶段,针对系统的初始状态和待验证的时序性质,对无穷状态系统的 CLP 规约进行特化;(2)第二阶段,采用自底向上策略对特化后的程序进行求值。该方法的有效性在很大程度上取决于程序特化阶段所采用的泛化策略。我们综合程序分析与程序变换领域已有的若干技术,组合得到多种泛化策略,并提出了一些新的策略。随后,通过大量验证实验,我们评估了所考虑的各泛化策略的有效性。最后,我们将基于特化的验证方法的实现与其他基于约束的模型检测工具进行了比较。实验结果表明,我们的方法与这些其他工具所采用的方法相比具有竞争力。将发表于《Theory and Practice of Logic Programming》(TPLP)。