时间Petri网的ECS-class可达性分析方法

时间Petri网(TPNs)是实时系统时间特性常用的描述和验证的Petri网模型,可达性分析是Petri网模型最基本分析方法.基于"状态类(State-class)"的可达性分析方法不能正确计算并发情况下的时间延迟,而基于"带时间戳的状态类(CS-class)"的可达性分析方法不能正确处理冲突情况下的事件调度,因此提出了"扩展的带时间戳的状态类(ECS-class)"可达性分析方法.它不仅正确的计算时间延迟,而且合理地调度事件.并对一个时间Petri网模型进行可达性分析验证.     

单触发Petri网的一个可达性判定方法

可达性判定问题是Petri网理论研究的一个重要课题.已有文献提出通过构造Petri网的可达树或可覆盖树来分析其可达性,但其中无界量ω的引入导致了无界Petri网运行过程中的信息丢失,使其可达性无法得到判定.众所周知,对于有界Petri网,通过构造其可迭性树或可达标识图来判定其可达性是容易的,但对于大量存在的无界Petri网,找到一个能判定其可达性的一般性算法却不太容易.本文给出一个Petri网子类--单触发Petri网,并给出它的一个可达性判定方法.     

一种新的混杂Petri网可达性分析方法

讨论混杂Petri网的标识可达性问题.以混杂Petri网模型行为演变为基础提出了一种新的可达性分析方法.根据混杂Petri网模型行为演变划分了混杂Petri网的四种演变类型,给出并证明了每一种演变类型的可达性判定定理,基于这些定理给出了相应的可达性分析算法.另外,与已有的方法进行比较分析,分析结果表明所提出方法的有效性.     

Petri网可达性的综合判定法

Petri网标识的可达性判定问题是进行Petri网分析的基础，而传统的判定方法并不能确保所得结果的可靠性．在揭示Petri网可达性问题的实质之后，讨论了在标识图的同一连通域内标识可达性的判定问题，进而在分析相关原理的基础上提出了一种有效判定Petri网标识可达性的“综合判定法”．此判定方法综合多种传统判定方法的优点，结合Grobner基理论，确保了对Petri网标识可达性进行判定所得结果的可靠性．     

时间Petri网弱语义模型的形式化分析

时间Petri网存在强语义和弱语义两种模型,弱语义模型更适合建模和分析外部环境触发的冲突选择问题,但其形式语义和可达性分析方面的研究,却很少有人问津。利用带标号的变迁系统定义时间Petri网弱语义模型的形式语义,采用时间戳状态类方法分析它的可达性,并证明了可达性问题的可判性和状态类时间戳的全局时间性质。     

Petri网可达性的伪标识判定法

Petri网标识的可达性判定问题是进行Petri网分析的基础。在分析目前现有的判定Petri网可达性的求解方法的基础上,提出一种伪标识判定法。该方法在状态方程法的基础上,利用关联矩阵来判断变迁发射向量是否能够发生来筛除伪标识。通过对实例的求解说明了求解过程并证明了算法能够确保对所得结果的可靠性,减少了算法的时间复杂度。     

时间约束Petri网的状态可达及可调度分析算法

时间约束Petri网是具有广义时间约束的一类Petri网。时间约束的引入使TCPN’s的演化与系统每一时刻的状态密切相关,导致网的动态复杂性。目前有关TCPN’s状态可达性的研究仅局限于一些较简单的网,该文通过对TCPN’s的进一步研究,给出了更一般的可达性分析方法及变迁可调度决策算法,并讨论了含冲突结构的TCPN’s的可调度分析。     

基于着色Petri网仿真模型的安全协议分析

采取形式化方法验证协议的安全性,Petri网是有效的方法之一,但传统Petri网分析过程中经常会出现状态空间爆炸问题。该文采用了基于着色Petri网建立安全协议及入侵者攻击的仿真模型方法,从而获得仿真数据。该方法利用逆向状态分析和Petri网可达性分析,能有效地发现协议中的安全漏洞。并且,如果能恰当地控制好状态空间,则能有效地克服Petri网分析过程中的状态空间爆炸问题。该文给出的利用着色Petri网建立安全协议仿真模型分析的一般方法,实例说明该方法具有普适性,并且方便利用Petri网自动化分析工具实现自动化分析。     

基于时间Petri网的舰空导弹发射控制软件安全性分析

文中借助时间Petri网出色的图形表达能力和对动态行为的描述,在Tina工具辅助下完成了对舰空导弹发射控制软件建模和安全性分析,分析了高风险状态的可达性,考虑到软件时效对安全性的影响,提出了一些改进建议以避免高危状态的出现。     

Petri网连接过程中的行为关系

先前的Petri网模型的综合研究着重在性质的保持性方面,象活性、可达性和回归性. 然而,系统行为关系的保持性研究应该更为重要.本文研究了Petri网模型自环连接、抑止弧连 接和同步连接三种操作的行为关系,获得他们的语言关系公式,这些结果为Petri网模型综合过 程中的动态行为分析提供了形式工具.     

Reachability analysis of real-time systems using time Petri nets

Time Petri nets (TPNs) are a popular Petri net model for specification and verification of real-time systems. A fundamental and most widely applied method for analyzing Petri nets is reachability analysis. The existing technique for reachability analysis of TPNs, however, is not suitable for timing property verification because one cannot derive end-to-end delay in task execution, an important issue for time-critical systems, from the reachability tree constructed using the technique. In this paper, we present a new reachability based analysis technique for TPNs for timing property analysis and verification that effectively addresses the problem. Our technique is based on a concept called clock-stamped state class (CS-class). With the reachability tree generated based on CS-classes, we can directly compute the end-to-end time delay in task execution. Moreover, a CS-class can be uniquely mapped to a traditional state class based on which the conventional reachability tree is constructed. Therefore, our CS-class-based analysis technique is more general than the existing technique. We show how to apply this technique to timing property verification of the TPN model of a command and control (C2) system.     

Relevant Timed Schedules/Clock Vectors for Constructing Time Petri Net Reachability Graphs

We consider here the time Petri nets (the TPN model) and its state space abstractions. We show that only some timed schedules/clock vectors (one per enabled transition) of the clock/firing domains are relevant to construct reachability graphs for the TPN. Moreover, we prove formally that the resulting graphs are smaller than the TPN reachability graphs proposed in the literature. Furthermore, these results establish a relation between dense time and discrete time analysis of time Petri nets and allow also improving discrete time analysis by considering only some elements of the clock/firing domains.     

Compositional schedulability analysis of real-time systems using time Petri nets

This paper presents an approach to the schedulability analysis of real-time systems modeled in time Petri nets by separating timing properties from other behavioral properties. The analysis of behavioral properties is conducted based on the reachability graph of the underlying Petri net, whereas timing constraints are checked in terms of absolute and relative firing domains. If a specific task execution is schedulable, we calculate the time span of the task execution, and pinpoint nonschedulable transitions to help adjust timing constraints. A technique for compositional timing analysis is also proposed to deal with complex task sequences, which not only improves efficiency but also facilitates the discussion of the reachability issue with regard to schedulability. We identified a class of well-structured time Petri nets such that their reachability can be easily analyzed.     

Verifying time Petri nets by linear programming

The paper proposes an approach to solving some verification problems of time petri nets using linear programming.The approach is based on the observation that for loop-closed time Ptri nets,it is only necessary to investigate a finite prefix of an untimed run of the underlying Petri net.Using the technique the paper gives solutions to reachabiltiy and bounded delay timing analysis problems.For both problems algorithms are given,that are decision procedures for loop-closed time Petri nets.and semi-decision procedures for general time Petri nets.     

基于Petri网的Web服务流语言(WSFL)建模与分析

描述了Web服务流语言(WSFL)的Petri网建模方法，利用网结构描述商业流程基本结构。在对WSFL的语法元素进行分析的基础上，有效地对WSFL所描述的商业流程进行了Petri网建模。在此基础上，结合Petri网的可达图分析技术，分析和验证了商业流程的可达性和活性等性质。     

Petri网的标注可达

本文基于Petri网的可达树的概念,给出标注可达树定义,并且证明网N与其标注可达树是一一对应的,然后,我们给出了网N与相应的标注可达树的相互转换算法。     

An Improved Approach to Test Diagnosability of Bounded Petri Nets

For bounded Petri nets, Cabasino et al. propose a diagnosability test method that is based on the analysis of a modified basis reachability graph and a basis reachability diagnoser. However, its complexity is exponential in the number of nodes of the basis reachability diagnoser. In order to reduce the complexity of their method, this paper presents a new diagnosability test approach for bounded Petri nets. We present the concept of an extended basis reachability graph and prove that our approach is of polynomial complexity in the number of nodes of extended basis reachability graphs. An example is given to illustrate the application of the presented approach.      

基于约束优化的Petri网可达性分析

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

Petri网仿真和自动化分析中的存储结构及算法研究

存储结构及算法是Petri网仿真和自动化分析研究中的重要内容，Petri网是一种特殊的有向图，通过对图的存储问题进行研究，提出了一种有向图的存储结构-树链式结构，给出了其构造算法，与其它有向图存储结构相比，它既可提高算法速度又能降低算法复杂性，树链式结构在Petri网仿真和自动化分析中应用优势明显，着重讨论了Petri网的树逻式存储结构，提出了基于该存储结构的可达树生成算法，所生成的可达树的树链结构形式，利于展开Petri网的各种分析算法。     

移动网可达树

随着计算机技术和网络通信技术的高速发展,对于并发分布式系统,已经提出了进程代数以及Petri网等形式化分析方法。近年来由于移动互联网的出现和快速发展,通过在进程代数中增加移动性得到了pi演算,与此同时,Petri网领域也采用谓词/变迁网、颜色网等构建移动系统模型。但它们仍存在一些不足之处。在此基础上,A.Asperti和N.Busi提出了移动网这一系统模型。移动网是在Petri网的基础上增加了移动性并结合了进程代数的优势得到的,适用于描述和刻画移动计算系统。然而,目前并没有对于移动网相应分析方法的研究。为此开展了移动网模型分析方法的研究,给出了移动网可达树的构造算法,提供了移动网模型可达性分析方法,并对移动车辆电话通信系统实例进行了分析。