合成Petri网P不变量的性质分析

针对Petri网两种合成操作(共享合成、同步合成),采用组合原Petri网不变量生成合成Petri网不变量的方法,研究了合成Petri网P不变量的变化规律。对于同步合成Petri网,当原Petri网邻接矩阵的秩不超过各自转移数与共享转移数的差时,合成网的P不变量可以用原网P不变量的线性组合表示。对于共享合成Petri网,网的P不变量的位置投影是原网的P不变量;当原Petri网的P不变量线性相关时,可用其线性组合表示合成网的P不变量。     

基于广义随机Petri网的SIP的验证和性能分析

在给出会话初始化协议（SIP）的服务工作过程的基础上,建立了SIP的广义随机Petri网模型（GSPN）,利用广义随机Petri网坚实的数学基础和分析技术完成对会话初始化协议的分析验证和性能分析。通过可达性分析、S_不变量分析和T_不变量分析验证了会话初始化协议的有界性、活性、守恒性和循环性。并且构造出与广义随机Petri模型同构的马尔可夫链,基于马尔可夫链的稳定状态概率进行系统性能分析。对会话初始化协议相关研究以及解决实际问题具有一定的理论价值。     

求取S-不变量基的新算法

S-不变量是进行Petri网结构性质分析的重要工具,但S-不变量的求取尚无有效算法。作者在S-不变量的极小支集的判定、极小支集上S-不变量的求取等方面创新性地提出了一些多项式解决算法。将在上述工作的基础上,结合枚举思想给出一个求取S-不变量基的算法,并提出一些筛选规则以提高枚举的性能。     

不可否认协议形式化分析的Petri网方法

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

基于T-不变量的可重复向量的求解算法

研究了Petri网中T-不变量与可重复向量之间的关系,并基于此关系给出一个求解可重复向量的新方法。首先定义了变迁扩充网的概念,证明一个网的可重复向量与其变迁扩充网的T-不变量之间存在一一对应关系,从而将一个网可重复向量的求解转换为其变迁扩充网T-不变量的求解上。在此方法中,如果利用FM-算法去求解T-不变量,则某些求解的步骤可以省略,从而得到一个类似于FM-算法的算法来求解可重复向量。此算法能够求出一组可重复向量,而任一可重复向量都可被这组可重复向量非负有理系数线性表出。     

从协议Petri网到Estelle的转换

Petri网和Estelle是国际上流行的两种描述通信协议的形式技术.基本Petri网及其衍生变种具有图形的直观表示和数学的分析方法,在协议工程领域有着广泛的应用.而Estelle类似于程序语言,可对协议进行无二义的描述.本文针对现有Petri网系统的不足,从协议形式描述的角度出发,定义了一种抽象通信特性的协议Petri网,给出了由协议Petri网转换为Estelle形式的方法.基于此方法文章还构造了自动实现转换的算法,并给出了一个实例.     

基于Petri网的双重数字签名的描述与验证

双重数字签名是保障电子交易中持卡人、商户及银行三方安全传输信息的重要技术之一。Petri网是一种描述和验证密码协议的有效手段。利用Petri网从静态和动态两方面仿真分析双重数字签名在电子支付系统中的应用。在静态描述方面,建立了双重数字签名的Petri网模型,并给出形式化描述。在动态验证方面,采用可达树分析此密码协议,验证了可达性、有界性、活性等性质。同时分析表明双重数字签名具有抵抗非法入侵的能力,可以提高电子支付系统的安全性。     

现场通信系统的仿真建模及其性能评价方法

由于Petri网适于描述系统冲突和竞争，故在较多场合中引入了Petri网对通信协议及系统进行建模，但目前采用Petri网对现场通信系统建模和评价还很少，通过Petri网协议描述实现现场通信和评价系统性能双重功能更无先例，本文在时间Petri网的基础上加以拓展，提出了现场通信协议的类时间Petri网描述方法，针对多协议现场通信控制装置FCCD，从理论上建立了FCCD系统的类时间Petri网模型，实现了多协议智能设备的互连及其系统的性能仿真评价。     

基于Petri网的一类调度问题的分层控制器设计

利用Petri网中T不变量的思想,针对约束为T不变量的Parikh向量形式的job-shop调度问题,提出了一种分层控制器的设计算法,该算法有效地解决了这一有并发约束的控制问题。即使随着系统规模的增大,该方法计算量仍然很小,而且与经典的库所不变量方法相比较,它不受有无自回路的约束,可有效地解决一类实际制造系统中的job-shop调度问题。     

基于有色Petri网的安全协议安全性仿真

如何验证安全协议的安全性是一项非常重要的工作。提出了一种基于有色Petri网的安全协议形式化描述与安全性仿真验证方法。给出协议的有色Petri网模型,分析协议运行过程中可能出现的不安全状态,利用Petri网的状态可达性判断这些不安全状态是否可达从而验证协议的安全性。针对Diffie-Hellman协议给出了具体的仿真分析过程,证明了这种方法的有效性。     

IPTV数字内容版权保护安全协议的设计

针对IPTV流媒体应用的特点,提出适应IPTV流媒体应用特点的适用于动态的、分布的、异构的、开放的网络环境下的数字版权保护协议,对网络中动态出现的内容服务提供了完善的数字版权保护功能,并具有跨网络安全域的特点。该协议在满足数字版权保护协议基本要求的同时,引入了版权中心和服务网关,以便更好地保证协议抗攻击的能力和内容提供者和消费者在版权方面的公平性。利用PETRI网的分析方法,对协议中各种变迁及状态变迁进行了分析。分析结果表明协议结果具有教强的安全性。     

基于模糊有色Petri网的不确定性学习和推理方法

模糊Petri网模型可以用于模糊推理,但在Petri网中不得不用独立子网表示所有类型的过程,即使这些过程具有相同的行为,这导致整个Petri网变得很大.文中提出基于模糊有色Petri网的不确定性推理方法和基于遗传算法的学习过程.在减少网络规模,计算时间和克服解释网络困难的同时,它能保持等量的信息,提供结构化的表示,使知识库中的规则之间的关系易于表示.     

基于随机Petri网的机载软件更新系统性能评价

近年来,航电系统发展的趋势由联合式航电系统向综合化航电系统逐步演进,许多应用将原来专用集成电路实现的功能采用软件实现。软件更新系统在机载航电系统中的地位日益重要。提出了一种高效机载软件更新系统OBSUS,并运用随机Petri网理论对其性能评价。首先,提出了OBSUS的系统结构与组件间的通信协议。其次,根据OBSUS的系统结构与通信协议,建立了系统的随机Petri网模型。最后,对随机Petri网模型进行了瞬态概率分析,针对影响系统的诸多因素,如flash芯片烧写时间、数据传输丢包率和数据传输速率等,对系统的综合性能的影响进行了量化分析。仿真研究结果对于机载软件更新系统的结构与数据传输协议设计,以及如何提高系统性能,具有较强的指导意义。     

BitTorrent协议的Petri网建模方法研究

BitTorrent协议被大规模文件共享、视频点播等P2P应用所广泛采用,但其交互行为复杂且并发度高,难以构建规模适度的形式模型以支持高效可行的协议功能行为分析。基于着色Petri网提出一种BitTorrent协议分层建模方法,给出协议的着色Petn网层次模型,集戍模拟、状态空间分析与模型检验等方法对模型的不同抽象层进行分析。确认协议模型有效性,并验证协议行为满足协议需求。BitTorrent协议的着色Petri网层次模型不但为协议开发提供准确、直观的形式规范说明,而且便于协议行为模拟和协议属性分析,有效缓解大规模系统建模分析过程中存在的状态爆炸问题。     

基于时间Petri网的电力系统故障恢复算法的研究

随着电网建设的逐步升级和加强,电网结构趋于成熟稳定,但也愈加庞大复杂。电网不可避免受到故障影响而导致停电,严重危害社会经济的持续发展,因此,电力系统故障恢复问题的研究正成为完善电网建设的一项重要任务。时间Petri网是一种用于描述系统动态行为和分析系统动态性质的数学模型,对描述和分析并发现象有其独到的优越之处,非常适合于异步并发系统的建模。用时间Petri网来解决故障恢复是一种新型算法。根据时间Petri网的特点,利用时间Petri网为配电网典型结构建立模型,应用迪杰斯特拉计算机算法,辅助计算电力系统配电网故障恢复的最优路径。举例验证本算法的有效性。     

电子支付协议可追究性的Petri网建模与分析

可追究性是电子支付协议必须满足的安全属性之一,针对电子支付协议,建立了支持支付协议可追究性分析的分层有色Petri网模型,并基于此提出一种对支付协议可追究性分析的一般性方法.Kungpisdan等人曾提出一种可追究性逻辑,证明一个典型的移动支付协议KSL协议满足可追究性.但使用上述所提方法对该协议建模并进行可追究性分析,发现了可追究性逻辑未发现的漏洞,分析例证结果表明了所提方法的有效性.