A Formal Model of OSI X.25/FR Gateway Based on High Level Petri Net

Specification and validation of protocol conversion in a gateway is a difficult problem in protocol engineering. During design and implementation of an OSI X.25/FR gateway, a high level Petri Net called EPr/TN is introduced as a formal specification tool to solve this problem. A formal model of the gateway is constructed by using Epr/TN. Based on this model, the process of protocol conversion and data transmission in the gateway are analyzed and validated. With object oriented techniques, this model is also utilized in the software development of the gateway.

基于Petri网的异构协议转换的构造

异构网络由于协议的不兼容造成异构网络应用进程之间难以通信，因此异构网络集成是当前网络工程所面临的困难之一．协议转换是实现异构网络互联的关键技术．文中首先给出协议转换的基本概念，并简述传统的协议转换方法．在此基础上，文中给出了基于Ｐｅｔｒｉ网的协议转换的定义，并利用Ｐｅｔｒｉ网的Ｔ不变量技术和并行组合积技术，按照自底向上的方法，提出了基于Ｐｅｔｒｉ网的协议转换器的构造算法及其证明，最后通过实例验证了其正确性和可行性．

多元化网络管理协议的Petri网模型及其验证(英文)

介绍了一种新型的卫星网网络管理协议,并阐述了此协议服务联系和服务原语的设计,利用Petri网描述协议的方法,对此网络管理协议模型进行了形式化描述,并利用Petri网的可达性分析、S_不变量分析和T_不变量分析对此协议进行了逻辑正确性验证,确保了此协议具有有界性、活性、守恒性、完整性、前进性等性质,从而减少了协议设计中潜在的错误,为此协议的实现打下了良好的基础。

基于高级Petri网的OSI网络协议描述与验证

本文对ＯＳＩ参考模型进行了全面的分析，并介绍了一种高级Ｐｅｔｒｉ网，称为ＥＰｒ／Ｔ网系统，该系统可作为ＯＳＩ网络协议的形式描述工具．然后，利用ＥＰｒ／Ｔ网系统对（Ｎ）层通信协议进行了形式描述，并阐明了ＯＳＩ网络协议形式描述的一般方法．最后，对协议的有界性。

用Petri网对点击拨号业务的建模

该文提出一种将协议转换方法学和Petri网理论相结合来研究应用层协议转换的新方法。按照协议转换方法学的流程,对IIN(Internet Intelligent Network)模型中的点击拨号(CTD)业务进行分析。在用Petri网对CTD业务的建模过程中提炼出通用的Petri网模型协议转换耦合原则,丰富了协议转换方法学的内容。利用Petri网的分析能力分析了CTD业务协议转换模型的特性,达到了检错纠错的目的。在该方法的指导下开发了业务控制网关(SCGF) 和CTD业务,证明了这种新方法的可行性和适用性。

移动环境下订阅分发协议的随机Petri网模型

针对移动环境下订阅分发服务的需求,提出了基于位置的订阅分发协议(LBPSP)。应用高级Petri网对LBPSP协议的核心操作进行建模,并对协议的正确性与异常处理完备性进行了验证。

虚拟接口体系结构的Petri网模型及分析

随着计算机硬件的发展,网络硬件支持Gb/s的带宽已成为现实。但是由于分层网络软件频繁的系统调用和内存-内存拷贝,物理层和应用层之间形成性能鸿沟。虚拟接口体系结构是一种崭新的机群系统内部通信思想,它为用户提供了一个直接与网络相联系的虚拟接口,使操作系统不参与进程双方的通信过程,大大提高了通信效率。首先介绍了虚拟接口体系结构,然后为Berkeley模型建立了Petri网模型,通过模型对其工作模式进行分析,并对其中存在的活锁问题给出了具有实际意义的解决方法。

网络传输层协议的随机Petri网模型及性能分析

描述了广义随机高级Petri网(GHLSPN)在计算机网络传输协议的模型与性能评价中的作用, 并对影响网络性能的系统指标进行了讨论；同时考虑了确认控制、窗口流控制和错误重传控制等机制对网络系统的性能影响，克服了以往对网络性能评估的某些局限。

基于对象Petri网的网络认证协议表示及分析

提出用对象Petri网表示网络认证协议的方法。这种方法能反映协议的动态特性，也利于体现协议执行主体可利用的资源。最后，总结出可把协议的安全性问题转化为Petri网单个位置的1-可达性问题。

从协议Petri网到Estelle的转换

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

基于高级Petri网的X.25/FR开放系统互连网关的描述与验证及实现

在构造 X.2 5 / FR互连网关时 ,采用 OSI有关协议。利用一种高级 Petri网(EPr/ TN)作为形式化的描述工具建立互连网关的系统模型 ,对网关中的协议转换和数据通信过程进行描述、分析和验证 。

从增强的LOTOS(E-LOTOS)说明到Petri网的转换

Ｅ－ＬＯＴＯＳ对ＬＯＴＯＳ的描述能力进行了多方面增强，Ｐｅｔｒｉ网是分析系统的有效工具，本文提出一种从Ｅ－ＬＯＴＯＳ说明到Ｐｅｔｒｉ网的转换方法。

基于Petri网的MMS服务描述、验证及实现

利用Ｐｅｔｒｉ网这一形式化描述工具建立了ＭＭＳ（制造报文规范）体系结构的抽象模型，并利用Ｐｒ／Ｔ网对其中的重要服务——程序唤醒服务进行了描述、分析和验证，最后，以此为基础在ＭＡＰ、ＢＩＴＢＵＳ网上实现了ＭＭＳ服务。

基于Petri网的带宽共享系统设计

针对局域内网单台计算机下载外网资源速度慢的问题,本文以Petri网为系统逻辑设计工具,提出一种基于P2P(Peer to Peer)分布式结构的外网带宽共享协议。该协议指定内网多台计算机在外网下载所需文件的不同片段,再由局域内网传输给任务发起者所属计算机进行原文件整合。协议充分利用多台计算机的并行下载能力以及局域内网的快速传输能力,从逻辑层面提高了单台计算机的下行带宽。本文进一步通过基于Petri网的可达标志图,S_不变量和流程图方法对协议的逻辑正确性和行为许可性进行了验证。

无线网络安全协议Kerberos的Petri网建模

由于无线网络与移动设备的特点,无线网络安全协议的执行环境变得更为复杂。对比了网络安全协议WAP、IEE802.1X、EAP、WPA认证协议和Kerberos协议。Kerberos协议在身份委派和身份验证方面较为高效,成为常用的无线网络安全协议。Petri网作为信息化建模仿真的常用工具,能以图形化、层次化的方式描述系统。在分析Kerberos协议工作原理的基础上,采用Petri网工具CPNTools对Kerberos协议进行建模与仿真,采用图形化方式,直观地表达了该协议特点。

基于带抑止弧时间Petri网的IEEE802.2LLC3型协议的建模

该文定义了一种扩展的时间Petri网———带抑止弧的时间Petri网,这类扩展的时间Petri网可以用作网络协议描述的工具。作为一个例子,笔者在对IEEE802.2LLC3型协议做简单分析的基础上,给出了一个基于带抑止弧时间Petri网的IEEE802.2LLC3型协议的形式描述。

Petri网在帧中继与X.25协议转换中的应用

提出了一种用Ｐｅｔｒｉ网研究两种协议转换的方法。在两个协议提供原语的基础上，利用Ｐｅｔｒｉ网丰富的描述特性建立转换模型，与用有限状态机建立转换模型相比，简化了过程。在Ｐｅｔｒｉ网的基础上，利用图论方法论证其正确性。最后，用这种方法分析了Ｘ２５与帧中继之间的协议转换，并建立转换模型。

WAP协议栈总体设计及WTP层的Petri网描述与实现

简介了 WAP协议并设计了实现该协议的总体方案 ,然后用 petri网的有关理论对 WTP层进行了描述 ,最后具体实现了

基于Petri网的战术互联网建模方法

为了兼顾建模仿真的实时性和精确性,在分析战术互联网结构和特点的基础上,提出一种基于Petri网的战术互联网建模方法,并从网络吞吐量和端到端时延2个方面进行了试验验证,对比分析表明:该方法易于实现,实时性高,在数据分组发送速率较低和节点运动速度较慢的情况下仿真精确度相对较高,能够较好地满足战术指挥模拟训练的需求。

基于着色Petri网的Web合成服务会话协议

基于着色Petri网的会话协议不仅能准确地描述Web服务的业务流程特征,而且具备强大的数据承载能力。该文以BPEL4WS语言为例,在对Web服务特性进行分析的基础上,给出了基于着色Petri网的会话协议以及相应的Web合成服务设计方法。通过这种框架,可以运用成熟的Petri网技术,对Web服务模型进行进一步的分析和验证,以提高服务的正确性和可靠性。