Under Consideration for Publication in Theory and Practice of Logic Programming Generalization Strategies for the Verification of Infinite State Systems
Under Consideration for Publication in Theory and Practice of Logic Programming Generalization Strategies for the Verification of Infinite State Systems
复制标题
正在考虑在逻辑编程的理论与实践中发表无限状态系统验证的泛化策略
DOI：
--
复制
发表时间：
--
期刊：
影响因子：
--
通讯作者：
V. Senni
中科院分区：
文献类型：
--
作者：
F. Fioravanti;A. Pettorossi;M. Proietti;V. Senni
我们提出了一种自动验证无限状态系统时间特性的方法。我们的验证方法是基于约束逻辑程序（CLP）的专业化，并分为两个阶段：（1）在第一阶段，无限状态系统的CLP规范在系统的初始状态和该系统的初始状态方面专门针对要验证的时间属性，（2）在第二阶段，使用自下而上的策略评估专业程序。该方法的有效性在很大程度上取决于在程序专业阶段应用的概括策略。我们考虑通过将在程序分析和程序转型领域中已知的技术组合在一起获得的几种概括策略，我们还介绍了一些新策略。然后，通过许多验证实验，我们评估了我们考虑过的概括策略的有效性。最后，我们将基于专业的验证方法的实现与其他基于约束的模型检查工具进行了比较。实验结果表明，我们的方法与这些其他工具使用的方法具有竞争力。
We present a method for the automated verification of temporal properties of infinite state systems. Our verification method is based on the specialization of constraint logic programs (CLP) and works in two phases: (1) in the first phase, a CLP specification of an infinite state system is specialized with respect to the initial state of the system and the temporal property to be verified, and (2) in the second phase, the specialized program is evaluated by using a bottom-up strategy. The effectiveness of the method strongly depends on the generalization strategy which is applied during the program specialization phase. We consider several generalization strategies obtained by combining techniques already known in the field of program analysis and program transformation, and we also introduce some new strategies. Then, through many verification experiments, we evaluate the effectiveness of the generalization strategies we have considered. Finally, we compare the implementation of our specialization-based verification method to other constraint-based model checking tools. The experimental results show that our method is competitive with the methods used by those other tools.