Petri网的反向展开及其在程序数据竞争检测的应用

• 作 者: 郝宗寅 鲁法明
• 机 构: 山东科技大学计算机科学与工程学院,厦门大学信息学院
• 出 处: 软件学报
• 发表日期: 2021年6期
• 关键词: PETRI网 可覆盖性判定 反向展开 启发式优化 数据竞争检测
• 基金项目: 国家自然科学基金(61602279,61472229),国家重点研发计划(2016YFC0801406),山东省泰山学者工程专项基金(ts20190936),山东省高等学校青创科技支持计划(2019KJN024),山东省博士后创新专项基金(201603056),鲁渝科技协作计划(cstc2020jscx-lyjsAX0008),国家海洋局海洋遥测工程技术研究中心开放基金(2018002),山东科技

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