摘要:近年来，基于Petri网可覆盖性的验证技术已经成功地应用于并发程序的验证与分析中.然而，由于Petri网的可覆盖性问题复杂度太高，这类技术在应用时有较大的局限性，对于输入规模较大的问题常常会出现超时的情况.而Petri网的一个子系统——非交互式Petri网，其可覆盖性和可达性复杂性均是NP完备的，同时表达力又可以作为某类并发程序的验证模型.设计并实现了可以高效验证非交互式Petri网可覆盖性的工具CFPCV.采用基于约束的方法，从模型中提取约束，并使用Z3 SMT求解器对约束进行求解，同时，通过子网可标记方法对候选解进行验证，从而保证每组解都是正确解.通过实验分析了该工具的成功率、迭代次数以及运行效率，发现该算法不仅验证成功率高，而且性能非常优异.



Abstract:In recent years, the verification technology based on Petri net coverability has been successfully applied to the verification and analysis of concurrent programs. However, due to the complexity of Petri net coverability, such technology has great limitations in application. For large scale input model, they all have timeout problem. While a subsystem of Petri net-communication-free Petri net, whose reachability and coverability are both NP-complete, can be used as a verification model of certain class of concurrent program because of its expression. In this study, a tool called CFPCV is designed and implemented, which can verify coverability of communication-free Petri net very efficiently. A constraint-based approach is used to extract the constraints from the model and solve the constraints with Z3 SMT solver, and then the candidate solutions are verified with subnet markable method to ensure that each solution is correct. The success rate, iteration times, and performance of the tool are experimentally analyzed, and it is found that the proposed algorithm has not only a high success rate but also excellent performance.



PDF全文下载地址:

http://jos.org.cn/jos/article/pdf/5750