一种多线程软件并发漏洞检测方法

多线程软件由于进程间共享使用资源而极易发生死锁这一严重的并发漏洞.通过Petri网模型对多线程软件进行建模,并利用混合整数规划技术检测其漏洞.目前,使用互斥锁的多线程软件可通过Gadara网建模和检测.而使用信号量的多线程软件,虽可用S*PR网建模,但是尚未有理论支撑混合整数规划用于其漏洞检测.定义了S*PR网的一个子类——SEM-S*PR网,它允许资源库所初始标志大于1且分支可对称地使用资源,进而可建模一类使用信号量的多线程软件.依据结构特点,证明了该网保持活性的充分必要条件是网运行过程中所有信标始终非空.此结论是混合整数规划用于SEM-S*PR网建模的多线程软件的并发漏洞检测的理论基础.     

一类活性Petri网控制器的冗余检测及结构简化

S4R(systems of sequential systems with shared resources)网是分析和解决柔性制造系统死锁现象常用的一种重要的Petri网子类模型,现有的基于S4R网的死锁预防方法通常采用对部分或者全部严格极小信标添加控制库所来实现.此类方法的不足在于得到的活性S4R控制器中往往存在冗余控制库所.针对已为网中每一个严格极小信标都逐一添加了控制库所和相关连接弧的活性S4R控制器,本文提出并设计了一种基于整数规划技术的冗余检测及结构简化方法,由此得到结构更简单、行为允许度更高的活性S4R控制器.该方法的核心思想是:如果网中已经存在一个p-不变式使得某个严格极小信标满足最大受控条件,那么为该严格极小信标添加的控制库所就是冗余的.由于该方法无需进行Petri网的可达性分析,避免了状态组合爆炸问题,因此具有较高的可行性和计算效率.最后用实验验证了本文方法的正确性和有效性.     

一种改进型的S4PR网活性条件

研究了顺序资源共享分配系统的建模模型S4PR (Systems of sequential systems with shared resources)网的活性问题. 已有的研究成果表明, 一个S4PR网在所有信标都满足max, max'或max"-controlled 时能保持活性, 但现有的活性条件对信标的限制严格且不适用于某些网系统, 本文提出了一类名为max*-controlled的改进型条件, 并证明了当一个S4PR网的所有信标都满足max*-controlled条件时, 网系统能保持活性. 与现有的其他条件相比, 新的活性条件更加宽松, 为设计更高允许度的死锁预防或者活性保持监控器提供了理论支撑.     

S4PR网的极小信标计算方法

为了解决S4PR网的信标求解问题,提出了一种计算网中全部极小信标的方法.该方法通过分析资源库所内工作环与资源库所集合之间的关系构建有向图（C-R图）,获取强连通的C-R子图集合,而每个C-R子图对应着一个信标,由此得到包含2个及2个以上资源库所的信标集合,将该集合与含有单个资源库所的极小信标集合进行并集运算,形成备选信标集合,通过算法对备选集合进行筛选,删除其中非极小的信标,进而得到网中全部的极小信标.该方法为获取S4PR网中全部的极小信标提供了有效、可行的方案,为下一步设计最优活性控制器奠定了基础.一个可用S4PR网建模的柔性制造系统实例验证了该极小信标计算方法的正确性.