Petri网模型的FTA安全性分析

故障树分析法(FTA)用于静态分析系统失效的可能事件和状态，是分析安全苛求系统可靠性和安全性的一种有效方法。Petri网是并发系统有效的描述和分析工具，但Petri网自身的分析方法无法严格证明其模型满足模拟的系统安全性。该文提出一种用于Petri网模型的安全性分析方法，有效地结合故障树分析法和Petri网可达图分析的各自优点，并实际应用于联锁逻辑模型的安全性分析。     

Petri网的进程文法和进程语言

一、引言 Petri网进程是分析网系统运行行为最有力的工具。Petri网进程既考虑了网系统的状态变化又准确记录了引起这些变化的条件,清晰地反映事件(变迁)之间的并发和顺序关系,因此,Petri网进程比其它分析方法更便于对并发现象以及系统中同并发有关的一些性质进行分析。然而,Petri网的一个进程只能反映Petri网的一种可能的运行情况。一个Petri网往往有许多个进程,不可能一一列举,这就为进程分析带来了困难。文[1,2]中,提出了利用进程表达式描述Petri网的所有进程的方法,一个有界Petri网的进程表达式是该网的基本子进程集(有限集)为字母表的正规表达式,一个无界公平Petri网在可重复进程段行为等价的条件下也是一个正规表达式。对     

基于Petri网的模型检测研究

模型检测是关于系统属性验证的算法和方法.它通常采用状态空间搜索的方法来检测一个给定的计算模型是否满足某个用时序逻辑公式表示的特定属性.系统模型的状态空间的爆炸问题是模型检测所面临的主要问题,其主要原因是系统自身的并发特性和状态变迁的语义交织对基于Petri网的模型检测理论和验证技术进行了较为详细的研究,着重探讨了基于Petri网状态可达图的偏序简化和偏序语义技术、基于自动机的模型检测算法、基于Petri网的状态聚合法以及基于系统对称性的参数化和符号模型检测技术，并给出了研究思路以及未来所要进行的重点研究工作.模型检测技术已在通信协议和硬件系统的验证等领域得到成功应用，并且随着各种状态空间简化技术和模型检测算法的不断优化，其在其他应用领域也展示出广泛的应用前景.     

基于Petri网展开的多线程程序数据竞争检测与重演

数据竞争是多线程程序的常见漏洞之一,传统的数据竞争分析方法在查全率和准确率方面难以两全,而且所生成检测报告难以定位漏洞的根源.鉴于Petri网在并发系统建模和分析方面具有行为描述精确、分析工具丰富的优点,提出一种基于Petri网展开的新型数据竞争检测方法.首先,对程序的某一运行轨迹进行分析和挖掘,构建程序的一个Petri网模型,它由单一轨迹挖掘得到,却可隐含程序的多个不同运行轨迹,由此可在保证效率的同时降低传统动态分析方法的漏报率;其次,提出基于Petri网展开的潜在数据竞争检测方法,相比静态分析方法在有效性上有较大提升,而且能明确给出数据竞争的产生路径;最后,对上一阶段检测到的潜在数据竞争,给出基于CalFuzzer平台的潜在死锁重演调度方法,可剔除误报,保证数据竞争检测结果的真实性.开发相应的原型系统,结合公开的程序实例验证了所提方法的有效性.     

Petri网的符号ZBDD可达树分析技术

Petri网是一种适合于并发系统建模、分析和控制的图形工具.可达树是Petri网分析的典型技术之一,它通过标识向量集合表征系统的状态空间,组合复杂性严重制约了该分析技术可处理系统问题的规模.零压缩决策图(Zero-Suppressed Binary Decision Diagrams,ZBDD)是一种新型的数据结构,是表示和处理稀疏向量集合的一种有效技术.文章基于Petri网町达标识向量的稀疏特征,给出了Petri网分析的符号ZBDD技术,该技术通过对标识向量(状态)的布尔向量表示、可达标识向最(状态)的符号ZBDD生成,实现Petri网可达状态空间的高效符号操作和紧凑符号表示.实验表明,基于ZBDD的符号可达性分析算法能够有效处理较大规模Petri网问题.     

不可否认协议的Petri网建模与分析

Petri网是一种描述及分析并发行为的工具,在安全协议的形式化分析中得到了广泛的应用．作为一种特殊的安全协议,不可否认协议虽然已得到了多种形式化方法的分析,但还没有人使用Petri网来分析它们．以一般安全协议的Petri网分析方法为基础,提出了使用Petri网分析不可否认协议的建模及分析方法,该方法可以描述并分析一些其他形式化方法无法描述的协议性质．使用该方法分析Zhou和Gollmann于1996年提出的一个公平不可否认协议,可以发现该协议的一个许多其他形式化方法不能发现的已知缺陷．     

装备维修保障的随机Petri网模型及分析

建立了装备维修保障系统的随机Petri（SPN）模型，应用SPN与马尔可夫链理论相结合的分析方法。为维修保障系统性能评估提供了理论依据。最后，通过实例分析了系统状态空间、各状态在稳态下的期望概率、系统可靠性和维修人员的工作强度。实例表明，相比传统的Petri网建模方法，在分析装备维修保障各状态间的逻辑关系和系统动态过程中，SPN具有显著的有效性和优越性。     

基于Petri网化简技术的工作流过程模型结构验证

目前,工作流系统向大型化发展,这使得基于可达图的验证技术在对大型模型进行验证时面临着状态空间爆炸的问题.因此,在过程验证之前,对大型模型进行化简是必要的.文中介绍两种化简规则.这些规则将一个大的Petri网化简为更小的Petri网,同时保持合理性属性,保证化简后的Petfi网和原有的Petri网具有相同的属性.介绍了Petri网、Workflow Petri网和过程合理性定义;讨论了针对Petri网的两种化简技术;提出了工作流过程模型结构合理性验证过程.     

一种基于Petri网的隐蔽信息流分析方法

隐蔽信息流分析是开发高等级可信计算机系统必须面对的问题.以Petri网作为开发安全系统的形式化建模工具,给出Petri网中隐蔽信息流存在的判定条件.提出该条件成立的两种网结构,进而可以在语法层次上预先判断隐蔽信息流的存在性,并使由此类结构引起的隐蔽信息流在系统的设计阶段得以避免.开发了一种基于Petri网可达图的隐蔽信息流存在性判定算法,算法遵循无干扰方法的思想,但是避免了无干扰方法中等价状态的区分和展开定理的使用.另外,算法采用深度优先搜索的策略,避免了Petri网全局可达图的构造.对复杂的安全系统,分析了子系统的各种组合运算对隐蔽信息流存在性的影响,降低了大规模系统分析的复杂度.     

基于CPEBSDL通信协议的Petri网建模方法

结合CPEBSDL描述语言、Petri网可达图、Petri网进程等协议分析方法,提出一种基于通信协议建立Petri网模型的方法——PMA_CPEBSDL。该方法利用CPEBSDL语言描述了通信协议实体的行为,自动地对协议建立Petri模型。协议的进程分析方法和可达图分析方法使协议的测试更加准确、直观。结合一个实例,给出LAPD协议完整的建模过程及协议验证和测试的方法。     

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.     

A technique of state space search based on unfolding

Unfoldings of Petri nets provide a method of searching the state space of concurrent systems without considering all possible interleavings of concurrent events. A procedure is given for constructing the unfolding of a Petri net, terminating the construction when it is sufficient to represent all reachable markings. This procedure is applied to hazard and deadlock detection in asynchronous circuits. Examples are given of scalable systems with exponential size state spaces, but polynomial size unfoldings, including a distributed mutual exclusion ring circuit.School of Computer Science, Carnegie Mellon University     

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网的反向展开及其在程序数据竞争检测的应用

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

线性定常系统的Petri网解耦控制

将Petri网与现代控制理论相结合,应用于连续系统的性能分析如可控性、可观性和稳定性等已日益普遍,但Petri网应用于系统的解耦控制研究很少.提出了广义连续自控网系统的形式化定义,描述了线性定常系统的广义连续自控网系统模型并分析了广义连续自控网系统模型与状态空间描述的等效性.基于状态反馈动态解耦的基本原理,探讨了利用Petri网模型结构实现线性定常系统解耦控制的新方法.该方法采用图的遍历算法,可有效的判断系统的可解耦性以及实现解耦控制律,避免了传统解耦控制方法中计算所需的大量矩阵运算.最后给出了两个具体的应用实例.     

Verification of bounded Petri nets using integer programming

Model checking based on the causal partial order semantics of Petri nets is an approach widely applied to cope with the state space explosion problem. One of the ways to exploit such a semantics is to consider (finite prefixes of) net unfoldings—themselves a class of acyclic Petri nets—which contain enough information, albeit implicit, to reason about the reachable markings of the original Petri nets. In [19], a verification technique for net unfoldings was proposed, in which deadlock detection was reduced to a mixed integer linear programming problem. In this paper, we present a further development of this approach. The essence of the proposed modifications is to transfer the information about causality and conflicts between the events involved in an unfolding, into a relationship between the corresponding integer variables in the system of linear constraints. Moreover, we present some problem-specific optimisation rules, reducing the search space. To solve other verification problems, such as mutual exclusion or marking reachability and coverability, we adopt Contejean and Devie's algorithm for solving systems of linear constraints over the natural numbers domain and refine it, by taking advantage of the specific properties of systems of linear constraints to be solved. Another contribution of this paper is a method of re-formulating some problems specified in terms of Petri nets as problems defined for their unfoldings. Using this method, we obtain a memory efficient translation of a deadlock detection problem for a safe Petri net into an LP problem. We also propose an on-the-fly deadlock detection method. Experimental results demonstrate that the resulting algorithms can achieve significant speedups.

Symbolic execution of concurrent systems using Petri nets

Techniques for analyzing sequential programs in order to improve their reliability have been widely studied in the past. Among the most interesting analysis techniques, we consider symbolic execution. However, analysis techniques for concurrent programs, and in particular symbolic execution, are still an open research area. In this paper, we define a method for symbolic execution of concurrent systems, based on an extension of the Petri net formalism, called EF nets. EF nets are a powerful, highly expressive and general formalism. Depending on the level of abstraction of actions and predicates that one associates to the transitions of the net, EF nets can be used as a high-level specification formalism for concurrent systems, or as a lower level internal representation of concurrent programs. Thus, the model is not dependent on a particular concurrent programming language, but it is flexible enough to be the kernel model for the representation of a wide set of systems and programming languages. In the paper, in order to support the analysis of a concurrent system or program, at first a general algorithm for symbolically executing an EF net is defined. Then, a more efficient algorithm is given for the particular, though important, subclass of EF nets, defined as safe EF nets. Such algorithm is proved to significantly help in reducing the amount of information needed to characterize a symbolic execution. Both the modelling power of the EF nets and the usefulness of the concurrent symbolic execution algorithms defined are illustrated by means of a case study.     

基于Petri网的并发程序测试用例产生方法

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

Automated generation of a progress measure for the sweep-line method

In the context of Petri nets, we propose an automated construction of a progress measure which is an important pre-requisite for a state space reduction technique called the sweep-line method. Our construction is based on linear-algebraic techniques concerning the transition vectors of the Petri net under consideration. We further discuss the possible combination of the sweep-line method with other state space reduction techniques (partial order reduction, the symmetry method).     

模糊Petri网知识表示方法在入侵检测中的应用

根据网络攻击具有并发性,攻击特征的提取具有不确定性等特点,给出了采用模糊Pelri网实现攻击知识的表达和入侵检测的推理模型。该模型解决了误用入侵检测系统中现有知识表示方法不能并行推理的问题,以及传统的基于Pelri网可达图搜索求解导致模型描述复杂、推理缺少智能的问题。最后通过入侵实例验证了该模型的正确性和有效性。