检索结果-南通市图书馆

基于程序运行轨迹Petri网模型挖掘的死锁检测方法

在线全文

学校读者我要写书评

暂无评论

计算机集成制造系统 2021年第9期27卷 2611-2624页

作者：鲁法明崔明浩包云霞曾庆田段华山东科技大学计算机科学与工程学院山东青岛266590 山东科技大学数学与系统科学学院山东青岛266590

程序死锁检测对于保证软件系统的稳定性具有重要作用。动态死锁分析方法由于具有高效和低误报率的特点而得到广泛研究。然而,传统的动态分析方法采用锁图及其各类扩展模型进行程序运行轨迹的建模和分析,它们难以对锁的授权/释放操作及... 详细信息

程序死锁检测对于保证软件系统的稳定性具有重要作用。动态死锁分析方法由于具有高效和低误报率的特点而得到广泛研究。然而,传统的动态分析方法采用锁图及其各类扩展模型进行程序运行轨迹的建模和分析,它们难以对锁的授权/释放操作及其执行场景进行准确刻画,从而会导致误报现象。针对该问题,提出一种新型的基于程序运行轨迹Petri网模型挖掘的多线程程序动态死锁分析方法。首先,捕获程序运行轨迹中各类并发原语对应的操作,并据此构建程序的Petri网模型;然后,将程序的死锁检测问题转化为程序伴随Petri网模型的死标识检测问题;最后,在传统可达树基础上,计算并扩充了可用于死锁重演的程序调度方案。所提方法能排除更多的误报,并给出一种确定性的死锁重演方案,可有效提高死锁检测的准确性。

关键词：程序运行轨迹死锁检测 Petri网死锁重演过程挖掘

在线全文

学校读者我要写书评

暂无评论

带有启发式因子的死锁模型检测算法

重庆理工大学学报（自然科学） 2022年第12期36卷 305-312页

作者：王焱吴涛杨斐成都信息工程大学计算机学院成都610225 中国核动力研究设计院核反应堆系统设计技术重点实验室成都610041

提出了一种基于差分进化算法的模型检测算法,用以解决模型检测中的死锁检测问题。模型检测方法通过抽象出一个系统的模型和定义关于该系统的具体规范,模型检测器就可以自动验证系统是否满足规范。由于一般的显式模型检测器是采用确定性... 详细信息

提出了一种基于差分进化算法的模型检测算法,用以解决模型检测中的死锁检测问题。模型检测方法通过抽象出一个系统的模型和定义关于该系统的具体规范,模型检测器就可以自动验证系统是否满足规范。由于一般的显式模型检测器是采用确定性算法来完成检测的(如深度优先搜索),因此在对状态空间较大的系统进行检测时,模型检测的效率较低,甚至不能完成检测。为了缓解这种问题,提出了一种基于差分进化算法的启发式模型检测算法。同时基于原有算法框架扩展了基于路径的编码、模拟退火、关键参数自适应等操作用于提高算法表现。结果表明,该算法可以在较少的时间内找到含有死锁状态的反例路径,并且与确定性算法和2种不确定性算法(粒子群算法,遗传算法)比较,在状态搜索方面与生成反例长度方面均有更好的表现。

关键词：模型检测差分进化算法死锁检测

基于混合整数规划的一般Petri网死锁检测方法

在线全文

学校读者我要写书评

暂无评论

控制理论与应用 2015年第3期32卷 374-379页

作者：庄巧莉戴文战王寿光浙江理工大学信息学院浙江杭州310018 浙江工商大学信息与电子工程学院浙江杭州310018

信标的受控性是检测柔性制造系统(flexible manufacturing system,FMS)Petri网模型是否存在死锁的关键因素.对于普通Petri网,在任何可达标识下所有信标不被清空是检测网系统非死锁的充分条件.然而,该条件对于建模能力更强的一般Petri网... 详细信息

信标的受控性是检测柔性制造系统(flexible manufacturing system,FMS)Petri网模型是否存在死锁的关键因素.对于普通Petri网,在任何可达标识下所有信标不被清空是检测网系统非死锁的充分条件.然而,该条件对于建模能力更强的一般Petri网并不适用,max可控性条件由此产生.研究证明,该条件对于一般Petri网的死锁检测过于严格了.虽然其后有很多研究者通过改进max可控性条件以求给出条件更宽松的一般Petri网非死锁的充分条件,但大部分的研究成果都仅仅局限于一种顺序资源共享分配系统Petri网模型S4PR(systems of sequential systems with shared resources)网.因此,本文在max可控性条件的基础上提出了新的名为max#可控的信标可控性条件,并在此条件的基础上实现了基于混合整数规划(mixed integer programming,MIP)的死锁检测方法.与现有研究成果相比,max#可控性条件更宽松,可适用于更多类型的一般网,为解决大规模柔性制造系统中死锁监督控制器的结构复杂性问题提供了有力的理论支撑.

关键词： Petri网柔性制造系统死锁检测混合整数规划

Petri网不可达标识的判定方法研究及其在死锁检测中的应用

在线全文

学校读者我要写书评

暂无评论

计算机集成制造系统 2016年第2期22卷 465-475页

作者：鲁法明曾庆田段华彭延军包云霞山东科技大学信息科学与工程学院山东青岛266590 同济大学嵌入式系统与服务计算教育部重点实验室上海200092 山东科技大学电子通信与物理学院山东青岛266590 山东科技大学数学与系统科学学院山东青岛266590

为进行系统死锁检测,对Petri网特定标识的不可达性判定方法进行研究。对基于虹吸管、陷阱、S-不变量、加模S-不变量等结构特性以及基于状态方程解存在性的不可达标识判定方法进行分析,研究了上述方法可以判定的不可达标识之间的相互关系... 详细信息

为进行系统死锁检测,对Petri网特定标识的不可达性判定方法进行研究。对基于虹吸管、陷阱、S-不变量、加模S-不变量等结构特性以及基于状态方程解存在性的不可达标识判定方法进行分析,研究了上述方法可以判定的不可达标识之间的相互关系,建立了Petri网不可达标识的分类体系,为更好地进行标识不可达性判定提供了理论依据。分别结合哲学家就餐问题和一个跨组织协同业务流程Petri网模型的死锁状态,检测说明了标识不可达判定方法的应用。

关键词： Petri网可达性分析不可达标识分类死锁检测

片上网络中基于拓扑排序的死锁检测与恢复方法

在线全文

学校读者我要写书评

暂无评论

上海交通大学学报 2013年第1期47卷 92-97页

作者：乔寓然伍楠杨乾明文梅张春元国防科学技术大学计算机学院长沙410073

提出了一种将拓扑排序应用于片上网络的死锁检测与恢复的方法.利用片上网络线资源丰富的特点,使用专用线路采集并分析网络中各通道之间的依赖关系,快速确定处于死锁环路中的通道位置,并对死锁环路进行解锁.结果表明,所提出的方法简单有... 详细信息

提出了一种将拓扑排序应用于片上网络的死锁检测与恢复的方法.利用片上网络线资源丰富的特点,使用专用线路采集并分析网络中各通道之间的依赖关系,快速确定处于死锁环路中的通道位置,并对死锁环路进行解锁.结果表明,所提出的方法简单有效,可以支持各种路由算法,与广泛应用的死锁避免策略相比,其网络资源的利用率和网络性能有所提高,并具有一定的容错能力.

关键词：片上网络拓扑排序死锁检测死锁恢复

在线全文

学校读者我要写书评

暂无评论

基于深度优先搜索算法的操作系统死锁检测

电脑与信息技术 2024年第3期32卷 17-19,54页

作者：丁红霞泰州学院江苏泰州225300

操作系统在现代生活中扮演着至关重要的角色,它被嵌入各种物联网和各种规模的计算机中。操作系统提供的服务之一是为进程分配资源,在分配过程中,可能会出现死锁。因此,操作系统必须提供一个能够检查系统状态以确定是否发生了死锁的算法... 详细信息

操作系统在现代生活中扮演着至关重要的角色,它被嵌入各种物联网和各种规模的计算机中。操作系统提供的服务之一是为进程分配资源,在分配过程中,可能会出现死锁。因此,操作系统必须提供一个能够检查系统状态以确定是否发生了死锁的算法。对于单一实例的资源类型,可以用等待图模型来检测死锁。但是教材中一般没有算法描述,只说时间复杂度是O(n~2)。文章将深度优先搜索算法应用于等待图模型检测死锁,其时间复杂度是O(n+m)。

关键词：深度优先搜索死锁检测操作系统等待图模型

在线全文

学校读者我要写书评

暂无评论

基于静态分析的分布式数据库死锁检测方法

信息工程大学学报 2022年第3期23卷 331-336页

作者：李银萍安徽文达信息工程学院安徽合肥231201

由于当前使用的关联规则挖掘、支撑集融合检测方法受到空间爆炸问题影响,不能及时更新分布式数据库死锁集合,导致检测误差大等问题。因此,对基于静态分析的分布式数据库死锁检测方法进行了研究。对分布式数据库进行分析,及时更新分布式... 详细信息

由于当前使用的关联规则挖掘、支撑集融合检测方法受到空间爆炸问题影响,不能及时更新分布式数据库死锁集合,导致检测误差大等问题。因此,对基于静态分析的分布式数据库死锁检测方法进行了研究。对分布式数据库进行分析,及时更新分布式数据库死锁集合,静态分析分布式数据库空间爆炸问题,建立常微分方程,处理频繁访问分布式数据库行为的死锁集合。设计没有节点失效和有节点失效的死锁检测过程,完成分布式数据库死锁检测。由实验验证结果可知,该方法与实验数据最大误报误差为2个,具有精准的检测结果。

关键词：静态分析分布式数据库死锁检测空间爆炸常微分方程

在线全文

学校读者我要写书评

暂无评论

基于Petri网的多线程程序死锁检测

计算机工程 2016年第4期42卷 1-6页

作者：黄理顾乃杰曹华雄中国科学技术大学计算机科学与技术学院合肥230027 中国科学技术大学安徽省计算与通信软件重点实验室合肥230027 中国科学技术大学先进技术研究院合肥230027

针对并发程序中死锁检测困难的问题,基于Petri网对多线程程序进行死锁检测。定义抽象描述多线程程序中锁操作的Petri网模型,在现有基于混合整数规划(MIP)的死锁检测算法基础上,提出改进的MIP算法检测该模型中是否存在死锁。实验结果表明... 详细信息

针对并发程序中死锁检测困难的问题,基于Petri网对多线程程序进行死锁检测。定义抽象描述多线程程序中锁操作的Petri网模型,在现有基于混合整数规划(MIP)的死锁检测算法基础上,提出改进的MIP算法检测该模型中是否存在死锁。实验结果表明,改进MIP算法能够检测到Petri网模型中的死锁,与标志矩阵算法和可达图相比,处理大规模多线程程序时计算效率更高。

关键词：多线程程序锁操作 Petri网混合整数规划死锁检测

基于扩展CSP多线程形式化建模与死锁检测研究

在线全文

学校读者我要写书评

暂无评论

基于扩展CSP多线程形式化建模与死锁检测研究

作者：高飞太原理工大学

学位级别：硕士

随着POSIX多线程(POSIX Threads,Pthreads)广泛应用于各类复杂并发系统,由线程竞争资源或推进顺序不合适所引发的死锁问题变得越来越常见。死锁会造成多线程程序崩溃或非正常终止,对于安全性要求较高的行业会带来灾难性的后果,因此如何... 详细信息

随着POSIX多线程(POSIX Threads,Pthreads)广泛应用于各类复杂并发系统,由线程竞争资源或推进顺序不合适所引发的死锁问题变得越来越常见。死锁会造成多线程程序崩溃或非正常终止,对于安全性要求较高的行业会带来灾难性的后果,因此如何有效检测出POSIX多线程程序中潜在的死锁至关重要。近年来,主流的死锁检测方法主要有形式化模型静态死锁检测分析和动态死锁检测两种。相比动态死锁检测方法而言,基于形式化模型分析的静态死锁检测方法由于具备完善的数学理论并且可以在软件系统编译之前检测到程序中潜在的死锁,因此备受广大学者推崇。但是该方法仍存在以下几方面问题需要研究:(1)形式化语言和多线程程序语义描述存在很大偏差,不能直接实现多线程程序语义到形式化模型的映射;(2)使用形式化语言对多线程程序建模时,很容易造成模型过于庞大,以至于在模型检测阶段会产生状态空间爆炸;(3)难以对多线程程序指针建立等价语义的形式化模型。针对以上问题,本文基于扩展CSP(extended CSP,CSP#)提出了一种对POSIX多线程程序自动建模与死锁检测的新方法,主要从以下几方面开展研究:一、提出一种POSIX多线程程序映射为CSP#模型的方法。根据多线程程序与CSP#建模语言之间的联系,引入C++CSP框架语言作为“桥梁”,分别建立了多线程程序与C++CSP框架语言、C++CSP框架语言与CSP#模型之间的映射关系,实现了多线程程序到CSP#模型的等价语义映射。二、基于独立性变迁和迹理论提出了一种CSP#模型精简算法(Simplified CSP#Model Algorithm,SCMA),通过对CSP#模型的连续独立变迁进行合并,减少了模型变迁序列的数量,有效缓解了模型检测状态空间爆炸的问题。三、基于指针别名分析技术,提出了一种堆栈地址解引用等价替换算法(Stack Dereference Equivalent Replacement Algorithm,SDERA),通过SDERA算法对多线程程序进行预处理,解决了多线程程序与CSP#模型变量描述不一致的问题。同时,设计并实现了支持POSIX多线程程序的自动建模工具——thr2CSP#Tool,并使用PAT(Process Analysis Toolkit)工具自动对建立的形式化模型进行了死锁检测分析。基于代码规模均匀分布、使用Pthreads实现并发操作的考虑,本文选取了TCPerver、OpenSSL-服务端、threadpool、Pfscan、bzip2smp程序作为测试用例。分别对建模及模型检测进行了测试用例分析,实验结果表明,本文方法可以快速对多线程程序构建CSP#模型,并能有效检测出其中潜在的死锁,适用于大规模多线程程序的死锁检测。

关键词：多线程程序形式化建模扩展CSP PAT 死锁检测