软件学报

作者：郝宗寅，鲁法明

单位：郝宗寅，山东科技大学 计算机科学与工程学院, 山东 青岛 266590;厦门大学信息学院, 福建 厦门 36100511,鲁法明，山东科技大学 计算机科学与工程学院, 山东 青岛 26659002

关键词：Petri网;可覆盖性判定;反向展开;启发式优化;数据竞争检测

基金：国家自然科学基金（61602279，61472229）；国家重点研发计划（2016YFC0801406）；山东省泰山学者工程专项基金（ts20190936）；山东省高等学校青创科技支持计划（2019KJN024）；山东省博士后创新专项基金（201603056）；鲁渝科技协作计划（cstc2020jscx-lyjsAX0008）；国家海洋局海洋遥测工程技术研究中心开放基金（2018002）；山东科技大学领军人才与优秀科研创新团队项目（2015TDJH102）

展开技术借助分支进程可在一定程度上缓解Petri网性质分析中的状态爆炸问题.但展开网中仍然包含了系统的所有状态信息.某些应用问题仅需对系统特定状态的可覆盖性进行判定，以此为目标，有望缩减网系统展开的规模.为此，针对安全Petri网的可覆盖性判定问题提出了一种目标导向的反向展开算法，结合启发式技术缩减展开的规模，以此提高目标标识可覆盖性判定的效率.进而，将反向展开算法应用于并发程序的形式化验证，将并发程序的数据竞争检测问题转换为Petri网特定标识的可覆盖性判定问题.实验对比了正向展开与反向展开在Petri网可覆盖性判定问题上的效率，结果表明：当Petri网展开的正向分支较多时，反向展开相比正向展开具有更高的可覆盖性判定效率.最后，对影响反向展开效率的关键因素做了分析与总结.

来源：2021年第6期

《软件学报》期刊编辑部

查看软件学报杂志2021年第6期