增量、归纳的覆盖性
计算机科学中的逻辑
2013-02-25 v2
摘要
我们给出一个增量、归纳（IC3）过程来检查良结构迁移系统的覆盖性。我们的过程将有限状态硬件验证中成功应用的IC3安全验证过程推广到无限状态良结构迁移系统。我们证明，对于向下有限良结构迁移系统——其中每个状态下方有有限个状态——该过程是可靠、完备且终止的，该类包含Petri网扩展、广播协议和有损信道系统。我们实现了检查Petri网覆盖性的算法。我们描述了如何在不使用SMT求解器的情况下高效实现该算法。我们在标准Petri网基准上的实验表明，IC3在时间和空间使用上与基于符号反向分析或扩展-扩大-检查算法的最先进覆盖性实现具有竞争力。
引用
@article{arxiv.1301.7321,
title = {Incremental, Inductive Coverability},
author = {Johannes Kloos and Rupak Majumdar and Filip Niksic and Ruzica Piskac},
journal= {arXiv preprint arXiv:1301.7321},
year = {2013}
}
备注
Non-reviewed version, original version submitted to CAV 2013; this is a revised version, containing more experimental results and some corrections