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

郝宗寅; 鲁法明

首页> 中文期刊> 《软件学报》 >Petri网的反向展开及其在程序数据竞争检测的应用

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

开具论文收录证明 >>

期刊封面封底目录下载 >>

文献代查 >>

页面导航

摘要
著录项
相似文献
相关主题

摘要

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

著录项

来源
《软件学报》 |2021年第6期|1612-1630|共19页
作者
郝宗寅; 鲁法明;
展开▼
作者单位

山东科技大学计算机科学与工程学院山东青岛 266590;

厦门大学信息学院福建厦门 361005;

山东科技大学计算机科学与工程学院山东青岛 266590;

展开▼
原文格式 PDF
正文语种 chi
中图分类程序设计、软件工程;
关键词
Petri网; 可覆盖性判定; 反向展开; 启发式优化; 数据竞争检测;

相似文献

中文文献
外文文献
专利

1. 基于Adaboost模型的并发程序数据竞争语句级检测 [J] . 孙家泽 ,易刚 ,舒新峰 . 计算机工程 . 2021,第012期
2. 高精度的大规模程序数据竞争检测方法 [J] . 高凤娟 ,王豫 ,周金果 . 软件学报 . 2021,第007期
3. 基于Pi演算的Android多线程程序的数据竞争检测 [J] . 王涛 ,马川 . 广西师范大学学报（自然科学版） . 2020,第002期
4. 并发程序中数据竞争检测方法 [J] . 张杨 ,梁亚楠 ,张冬雯 . 计算机应用 . 2019,第001期
5. 并发程序数据竞争检测方法研究和分析 [J] . 操旺根 . 信息技术与信息化 . 2019,第012期
6. 并发程序数据竞争检测方法研究 [C] . Ai Jieqing ,艾解清 ,Huang Jutao . 中国电机工程学会第13届青年学术会议 . 2014
7. Java并发程序中数据竞争的静态检测工具的设计与实现 [A] . 操旺根 . 2020

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

摘要

著录项

相似文献

相关主题

期刊订阅