SAT-Solving the Coverability Problem for Petri Nets

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.     

基于Petri网的协同三维建模工作流模型研究*

通过分析大规模三维场景单机建模所面临的局限性问题,对三维场景协同建模理论进行了描述。结合workflow net的定义以及建立工作流模型的方法,采用基于Petri网扩展的、用于复杂工作流模型设计的建模方法建立协同三维建模的工作流模型,并通过Petri网相关理论分析得出所建模型具有可达性、有界性、活性,并且是安全可靠的,同时对系统中必须加以解决的并发问题进行了相关的探讨。     

基于Petri网的协议分析技术及工具

研究基于 Petri网的协议分析技术及工具并对要开发的协议分析器工具软件进行需求分析和人机交互界面设计 ,进而阐述该工具主要功能模块实现的思路和算法 ,并将其应用于对 AB通讯协议的描述和性能测试分析 ,表明所开发的工具的有效性     

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

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

Reverse Unfolding of Petri Nets and its Application in Program Data Race Detection

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.     

异步多进程时间自动机的可覆盖性问题

已有的实时系统模型无法动态创建新进程.为此,基于时间自动机模型,提出了异步多进程时间自动机模型,将每个进程抽象为进程时间自动机,其部分状态能触发新的进程.考虑到队列会导致模型图灵完备,进程都被缓存在集合中,但仍可建模许多实时系统.通过将其编码到可读边时间Petri网,证明了该模型的可覆盖性问题可判定.     

良结构下推系统的可覆盖性问题的下界

良结构下推系统是下推系统和良结构迁移系统的结合,该系统允许状态和栈字符是向量的形式,因而它们是无限的.状态迁移的同时允许栈进行入栈出栈的操作.它“非常接近不可判定的边缘”.利用重置0操作,提出了一个模型可覆盖性问题复杂度下界的一般性证明方法,并且证明了状态是3维向量的子集和一般性的良结构下推系统的可覆盖性问题分别是Tower难和Hyper-Ackermann难的.     

工作流业务规则语义的完整性验证技术

工作流模型的验证技术主要包括语法验证、结构验证和语义验证,其中语义验证是层次最高、最为严格的验证,验证的范围十分广泛,也是难点所在,目前尚缺乏有效的方法.而且,语义的正确性会影响工作流模型的控制逻辑.也是结构合理性的影响因素之一.从工作流模型表达的语义出发,通过分析工作流模型刻画的业务规则以及相应的约束集部分,基于对约束集语义的形式化,问题转换为对约束集语义的完整性验证.如果工作流模型中的条件节点所描述的约束集语义有遗漏、冗余或者无意义,也决定了模型错误的拓扑结构.提出全域覆盖性判定定理及基于判定树的验证算法.通过验证工作流业务规则语义的完整性,对工作流模型结构的合理性也给予了保证.这种验证方法具有很强的通用性.不依赖于具体的建模方法,适用范围广泛.     

基于触发序列集合的过程模型行为相似性算法

过程模型的相似性计算是业务过程管理中不可缺少的任务,广泛应用于组织合并、用户需求变更、模型仓库管理等多个场景.对基于主变迁序列的相似性度量方法 PTS进行研究,并提出了改进方案.通过定义完整触发序列表示模型行为,基于A*算法结合剪枝策略实现触发序列集合间的映射,进而完成模型相似性计算.实验结果表明:该方法较主流的基于模型行为相似性算法,计算合理性有很大提升.     

基于规范流网的Web服务行为适配方法研究

Web服务适配是面向服务计算领域的重要研究内容.针对现有服务行为建模和适配技术在循环服务行为、数据流建模和状态空间爆炸方面存在的问题,提出一种新的服务行为建模和适配方法,并结合实例阐述该方法如何以规范流网为基础,建模服务行为,构造服务行为的符号化可覆盖树,构建数据依赖关系和动作依赖关系,构建符号化执行轨迹适配器,直至最后完成服务行为适配的整个建模和适配过程.