非交互式Petri网可覆盖性验证的高效实现

• 作者: 丁如江 李国强
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 非交互式Petri网 可覆盖性 验证 模型检测 SMT求解器
• 年，卷（期）: 2019,（7）
• 所属期刊栏目: 软件形式化验证专题
• 页码范围: 1939-1952
• 页数: 14页
• 分类号: TP301
• 字数: 12173字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005750

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李国强	上海交通大学软件学院	13	44	4.0	6.0
2	丁如江	上海交通大学软件学院	1	1	1.0	1.0