软件学报

作者：丁如江,李国强

单位：丁如江，上海交通大学 软件学院, 上海 20024011,李国强，上海交通大学 软件学院, 上海 20024002

关键词：非交互式Petri网;可覆盖性;验证;模型检测;SMT求解器

基金：国家自然科学基金（61872232，61732013）

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

来源：2019年第7期

《软件学报》期刊编辑部

查看软件学报杂志2019年第7期