首页 | 本学科首页   官方微博 | 高级检索  
相似文献
 共查询到18条相似文献,搜索用时 171 毫秒
1.
郝宗寅  鲁法明 《软件学报》2021,32(6):1612-1630
展开技术借助分支进程可在一定程度上缓解Petri网性质分析中的状态爆炸问题.但展开网中仍然包含了系统的所有状态信息.某些应用问题仅需对系统特定状态的可覆盖性进行判定,以此为目标有望缩减网系统展开的规模.为此,本文针对安全Petri网的可覆盖性判定问题提出了一种目标导向的反向展开算法,结合启发式技术缩减展开的规模,以此提高目标标识可覆盖性判定的效率.进而,将反向展开算法应用于并发程序的形式化验证,将并发程序的数据竞争检测问题转换为Petri网特定标识的可覆盖性判定问题.实验对比了正向展开与反向展开在Petri网可覆盖性判定问题上的效率,结果表明,当Petri网展开的正向分支较多时,反向展开相比正向展开具有更高的可覆盖性判定效率.最后,本文对影响反向展开效率的关键因素做了分析与总结.  相似文献   

2.
Petri网的可达性判定问题是进行Petri网分析的基础。通过分析目前求解Petri网可达问题的判定方法和基于约束程序的Petri网可达问题判定方法,提出一种基于约束优化的Petri网可达问题判定方法,该方法是在状态方程法的基础上,利用约束程序寻求可行解,再利用优化求最优解,从而减少问题搜索的分支,达到减少状态方程的解空间的目的。最后通过实例的求解验证算法能够提高判定效率。  相似文献   

3.
杨启哲  李国强 《软件学报》2017,28(4):804-818
由于多栈的模型图灵等价,因此通用的异步通讯程序模型的验证问题不可判定.为此,基于Petri网,提出了一个新的模型通讯——通讯Petri网对异步通讯程序进行刻画,通过对输入通讯进行k-型限制,以及对每个栈进行基于正则语言泵引理的抽象,通过将这样限制下的模型编码到数据Petri网,证明了限制下的新模型可覆盖性可判定.  相似文献   

4.
并发程序验证的时序Petri网方法   总被引:10,自引:0,他引:10  
并发程序的设计、分析和验证已经成为计算机理论界基础理论研究的方向之一。Petri网和时序逻辑被认 为是探讨该问题较为有效的两个理论工具,但二者都有局限性。该文引用一种新网子类;时序Petri网,描述了并发程序的时序Petri网建模方法;利用网结构描述程序基本框架及保证语句的原子性,通过时序逻辑公式反映程序的共享逻辑变量的赋值变化及时序关系,从而有效地对基本网无法描述的并发程序进行了建模;在此基础上,结合Petri网的可达图分析技术和时序逻辑的演绎公式,分析和验证了并发程序的安全性和活性性质。  相似文献   

5.
苏杰  杨祖超  田聪  段振华 《软件学报》2023,34(7):3064-3079
模型检测是一种基于状态空间搜索的自动化验证方法,可以有效地提升程序的质量.然而,由于并发程序中线程调度的不确定性以及数据同步的复杂性,对该类程序验证时存在更为严重的状态空间爆炸问题.目前,大多采用基于独立性分析的偏序约简技术缩小并发程序探索空间.针对粗糙的独立性分析会显著增加需探索的等价类路径问题,开发了一款可细化线程迁移依赖性分析的并发程序模型检测工具CDG4CPV.首先,构造了待验证可达性性质对应的规约自动机;随后,根据线程迁移边的类型和共享变量访问信息构建约束依赖图;最后,利用约束依赖图剪裁控制流图在展开过程中的独立可执行分支.在SV-COMP 2022竞赛的并发程序数据集上进行了对比实验,并对工具的效率进行比较分析.实验结果表明,该工具可以有效地提升并发程序模型检测的效率.特别是,与基于BDD的程序分析算法相比,该工具可使探索状态数目平均减少91.38%,使时间和空间开销分别平均降低86.25%和69.80%.  相似文献   

6.
钱俊彦  黄国旺  赵岭忠 《计算机科学》2011,38(12):131-134,161
语义Web服务组合的形式化描述和验证,是保证组合服务能正确运行的重要前提基拙。首先描述基于答案集编程(Answer Set Programming)的OWL-S建模方法,并分析基于答案集编程建模的优势。然后给出OWL-S流程模型中几种控制结构到中间模型Petri网的映射,并提出由Petri网生成答案集编程的算法。同时将时态约束引入到 组合服务验证中,利用时态约束表达待验证性质,将验证问题转换为求解逻辑程序的答案集。最后通过一个具体的实例说明该方法的有效性。  相似文献   

7.
约束求解应用到程序分析的多个领域,在并发程序分析方面也得到了深入的应用.并发程序随着多核处理器的快速发展而得到广泛使用,然而并发缺陷对并发程序的安全性和可靠性造成了严重的影响,因此,针对并发缺陷的检测尤为重要.并发程序线程运行的不确定性导致的线程交织爆炸问题,给并发缺陷的检测带来了一定挑战.已有并发缺陷检测算法通过约减无效线程交织,以降低在并发程序状态空间内的探索开销.比如,最大因果模型算法把并发程序状态空间的探索问题转换成约束求解问题.然而,其在约束构建过程中会产生大量冗余和冲突的约束,大幅度增加了约束求解的时间以及约束求解器的调用次数,降低了并发程序状态空间的探索效率.针对上述问题,提出了一种有向图约束指导的并发缺陷检测方法 GC-MCR (directed graph constraint-guided maximal causalityreduction).该方法旨在通过使用有向图对约束进行过滤和约减,从而提高约束求解速度,并进一步提高并发程序状态空间的探索效率.实验结果表明:GC-MCR方法构建的有向图可以有效优化约束的表达式,从而提高约束求解器的求解速度并减少求解器的调用次...  相似文献   

8.
用静态分析方法对并发程序进行死锁检测通常比较困难,其原因是会遇到状态空间爆炸问题.文中针对作者曾提出的一种可有效避免状态爆炸问题的死锁检测方法,进行进一步实验验证.该方法的基本框架是首先将表示并发系统的离散Petri网模型连续化,得到一种新的连续Petri网模型;在此基础上,建立系统的常微分方程模型;通过分析常微分方程组的解来检测系统中是否存在死锁.与传统方法不同点在于:该方法不需要遍历状态空问,而是分析一组常微分方程组的解.为了减少在求解常微分方程模型过程中的计算机系统的开销,作者还采取了一系列优化策略.哲学家进餐问题被用来说明死锁检测的方法.大量的实验结果说明作者所提出的方法有着较强的静态分析能力.作为副产品,这种分析方法还可以用来判定系统的有界性.  相似文献   

9.
并发程序与并发系统可以拥有非常高的执行效率和相对串行系统较快的响应速度,在现实中有着非常广泛的应用。但是并发程序与并发系统往往难以保证其实现的正确性,实际应用程序运行中的错误会带来严重的后果。同时,并发程序执行时的不确定性会给其正确性验证带来巨大的困难。在形式化验证方法中,人们可以通过交互式定理证明器严格地对并发程序进行验证。本文对在交互式定理证明中可用于描述并发程序正确性的验证目标进行总结,它们包括霍尔三元组、可线性化、上下文精化和逻辑原子性。交互式定理证明方法中常用程序逻辑对程序进行验证,本文分析了基于并发分离逻辑、依赖保证逻辑、关系霍尔逻辑等理论研究的系列成果与相应形式化方案,并对使用了这些方法的程序验证工具和程序验证成果进行了总结。  相似文献   

10.
并发程序的测试路径具有不可预测性,而Pctri网在描述并发方面具有其它系统模型无法比拟的优势。因此通过Petri网来产生并发程序的测试路径:对有并发程序的源代码构造的Petri网模型进行图形矩阵转换;按照一定的规则得出相应的独立段组;合并独立段组得出网的独立段群,此独立段群即为该并发程序的测试路径。实验证明,将Petri网用于并发程序测试用的例生成降低了测试难度,提高了测试效率。  相似文献   

11.
The unfolding technique can partially alleviate the state explosion in Petri nets through branching processes. However, all states of a system are still contained in its unfolding net. To deal with some practical problems, only the coverability determination of a specific state is needed. In view of this, reducing the scale of the unfolding net is feasible. This study proposes a target-oriented reverse unfolding algorithm for the coverability determination of 1-safe Petri nets, which combines a heuristic technique to reduce the scale of unfolding nets, thereby improving the efficiency of coverability determination. Furthermore, the reverse unfolding is applied to the formal verification of concurrent programs, and their data race detection is converted into the coverability determination of a specific state in 1-safe Petri nets. The experiment compares the efficiency between forward nfolding and reverse unfolding in the coverability determination of a Petri net. The results show that when the Petri net has more forward branches than backward branches, reverse unfolding is more efficient than forward unfolding. Finally, the key factors influencing the efficiency of reverse unfolding are analyzed.  相似文献   

12.
SAT-Solving the Coverability Problem for Petri Nets   总被引:2,自引:0,他引:2  
Net unfoldings have attracted great attention as a powerful technique for combating state space explosion in model checking, and have been applied to verification of finite state systems including 1-safe (finite) Petri nets and synchronous products of finite transition systems. Given that net unfoldings represent the state space in a distributed, implicit manner the verification algorithm is necessarily a two step process: generation of the unfolding and reasoning about it. In his seminal work McMillan (K.L. McMillan, Symbolic Model Checking. Kluwer Academic Publishers, 1993) showed that deadlock detection on unfoldings of 1-safe Petri nets is NP-complete. Since the deadlock problem on Petri nets is PSPACE-hard it is generally accepted that the two step process will yield savings (in time and space) provided the unfoldings are small.In this paper we show how unfoldings can be extended to the context of infinite-state systems. More precisely, we show how unfoldings can be constructed to represent sets of backward reachable states of unbounded Petri nets in a symbolic fashion. Furthermore, based on unfoldings, we show how to solve the coverability problem for unbounded Petri nets using a SAT-solver. Our experiments show that the use of unfoldings, in spite of the two-step process for solving coverability, has better time and space characteristics compared to a traditional reachability based implementation that considers all interleavings for solving the coverability problem.  相似文献   

13.
Boundedness is one of the most important properties of discrete Petri nets. Determining the boundedness of a Petri net is usually done through building coverability graph or coverability tree. However, the computation is infeasible for complex applications because the size of the coverability graph may increase faster than any primitive recursive functions. This paper proposes a new technique to check the boundedness without causing this problem. Let a concurrent system be represented by a (discrete) Petri net. By relaxing the (discrete) Petri net to a continuous Petri net, we can model the concurrent system by a family of ordinary differential equations. It has been shown that the boundedness of the discrete Petri net is equivalent to the boundedness of the solutions of the corresponding ordinary differential equations. Hence, we can check the boundedness of a (discrete) Petri net by analyzing the solutions of a family of ordinary differential equations. A case study demonstrates the benefits of our technique.  相似文献   

14.
The administration of authorizations in an organization is a complex task. To ensure that tasks constituting the business processes are performed by authorized users, a proper authorization mechanism is required. Alturi and Huang have proposed a workflow authorization model and presented a color-timed Petri net based representation of their model. In this paper, we extend their model by using the colored Petri net formalism to model authorization management, security constraints like separation of duties, and role hierarchy in an elegant way to establish an integrated authorization management model. One of the great advantages of using Petri net formalism for system modeling is its strong mathematical foundation and the availability of a rich set of analysis techniques. Therefore, we will show in this paper the use of linear algebraic technique to analyze the reachable authorization states, and coverability graph to calculate the valid execution chains against the colored Petri net based workflow authorization management model.  相似文献   

15.
基于Petri网的RBAC策略验证的研究   总被引:5,自引:1,他引:5  
本文为RBAC模型提出了一个基于着色Petri网的策略规格说明和分析的架构.Petri网能够捕获基数、责任分离等约束,而且能对优先和依赖约束进行说明、使用Petri网的可达到性分析技术对RBAC策略进行正确性验证.  相似文献   

16.
Petri网是一种适合于描述异步并发现象的建模工具,具有坚实的理论基础和成熟的分析技术。本文将Petri网技术应用在卫生监督管理信息系统的工作流建模中,提出了完整的卫生监督管理信息系统工作流模型,并对该模型的合理性进行了论证。  相似文献   

17.
一种知识库校验工具PKBV的设计与实现   总被引:1,自引:0,他引:1  
张墨华  李伟华 《计算机应用》2006,26(2):465-0467
以Petri网建模基于规则的知识库,并据此开发出知识库校验工具PKBV,该工具通过对Petri网可达性及不变量的分析计算,来检查知识库中常见的完整性与一致性错误,针对具有多领域知识库的复杂系统,PKBV具有抽取多领域知识库之间的关联规则并进行校验的功能,满足了复杂知识系统的校验需求。  相似文献   

18.
王红英  张桂戌 《微机发展》2007,17(4):182-185
UML广泛应用于软件建模,但缺乏有效的模型检测的方法,使用形式化方法对UML模型进行分析,可以发现UML模型的设计问题,提高UML模型的质量。对象着色Petri网是一种拥有接口库所的模块化着色Petri网,既是一种图形化建模工具,又是具有严格的语法语义定义的形式化方法。通过引入事件托肯,改进了将UML模型转换为对象着色Petri网的方法,结合实例将UML状态图和协作图映射为对象着色Petri网模型。并用着色Petri网的方法和工具对模型进行了分析,验证了模型的一系列性质。  相似文献   

设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号