Verification of Session Initiation Protocol Using Timed Colored Petri Net

In this work, Session Initiation Protocol model is established by using Timed Colored Petri Nets (TCPN). SIP (Session Initiation Protocol) is a protocol developed to assist in providing advanced telephony services across the Internet. The Session Initiation Protocol (SIP) has become the quasi-standard for Voiceover-Internet Protocol (VoIP) communications. SIP is based on a client–server infrastructure in which user agents represent the end-terminals as clients, proxy servers handle SIP message routing between the user agents, and registrar servers store the client’s contact information into a location service. By use of timed color set and useful time attributes in tokens defined in CPN tools, timer and time-related problems of SIP are modeled and analyzed. Timer is an important part for SIP, especially the INVITE transaction.

从Petri网到形式描述技术和协议工程

协议是计算机网络的命脉 ,协议复杂性的提高导致了协议工程学科的出现 .该文首先分析了协议工程各项活动的内容、方法和相互关系 ,讨论了各种形式描述技术 ( formal description technique,简称 FDT)的特性及其优缺点 ,从而引出基于 Petri网理论的 FDT.该文说明了 Petri网作为协议描述技术的优势 ,指出当前基于Petri网的协议工程研究的难点 ,其中面向协议开发的网工具是一项重要的研究内容 .按照开放系统互连参考模型的层次 ,总结了国际上的研究进展情况 ,并阐述了未来的研究趋势 .最后从协议描述、协议验证与分析以及辅助测试与实现这 3个角度给出了基于

基于Petri网的多播组动态管理协议IGMP的形式化分析

文中在对IGMP详细的机制分析的基础上用扩展的库所 变迁网对其进行了形式化的描述 ,从而奠定了IGMP协议分析和具体实现的基础。

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

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

Petri网协议分析器

本文以基于Ｐｅｔｒｉ网的协议工程工作站为研究目标，阐述协议工程工作站的基本功能，简介ＥＰｒ／ＴＮ网系统，着重探讨作者实现的协议描述分析辅助工具ＰＥＳＡＴ的功能特点和实现技术，并以一个例子加以说明．最后作者指出ＰＥＳＡＴ的完善工作和理想协议工程工作站建立的前景．

基于着色解释Petri网的网络协议建模及协同仿真方法

为解决协议工程中协议形式化验证和仿真断裂的问题,结合着色Petri网和解释Petri网,构造出一种可建模复杂离散事件系统的着色解释Petri网。借助观察者模式,依据着色解释Petri网的特点,提出了一种具有通用性的与协议仿真工具协同工作的方法。作为对该方法的示例,采用着色解释Petri网对避免冲突的多路访问协议进行建模。在保证与OPNET仿真模型一致的基础上,通过着色解释Petri网与OPNET的协同仿真,改良了避免冲突的多路访问的功率控制算法。基于着色解释Petri网的协同仿真,第一次紧密连接了Petri网和通用协议仿真工具,对协议工程将起到重要作用。

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

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

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

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

基于CPN的车载网络无证书匿名认证和密钥协商方案研究

为了解决现有车载网络的认证方案中普遍存在密钥托管带来的缺陷,以及没有考虑计算受限电子控制单元(ECU)轻量级部署和安全快速认证的问题,首先,针对计算不受限的ECU网络,提出了一种无双线性配对的轻量级无证书匿名认证和密钥协商方案,该方案通过椭圆曲线密码体制安全构建认证密钥对,通过哈希函数和异或等轻量级方法实现匿名认证和密钥协商。然后,针对计算受限的ECU网络,提出了一种无证书批量验证方案来降低认证成本。最后,提出了一种基于有色Petri网(CPN)和Dolev-Yao攻击者模型的安全验证方法,对整体方案进行形式化安全性评估。安全评估和性能分析表明,所提方案能有效抵抗重放、伪装、篡改、已知密钥、已知特定会话临时信息攻击等多种不同类型的攻击,在保证多重安全属性的同时有较小的计算与通信成本。

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

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

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

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

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

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

Bi-PIM协议的原理分析及其Petri网模型

文章在对Bi-PIM协议的机制进行分析的基础上,用扩展的库所/变迁网对其进行形式化的建模,为其具体分析和实现奠定了形式化和自动化的基础。

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

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

一种新型的Petri网扩充模型及其在协议描述和验证中的应用

在数字Ｐｅｔｒｉ网（ＮＰＮ）的基础上，提出一种新型的Ｐｅｔｒｉ同扩充模型（ＮＰＮｃ）。它与ＮＰＮ相比，具有更强的描述能力，能用于复杂协议的描述。此外，本文还提出非环协议概念，并对Ｐｅｔｒｉ同理论中适当终结、活跃等概念进行了扩充修改。文中后部以ＯＳＩ会话协议为例说明ＮＰＮｃ模型在协议描述和验证中的应用。

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

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

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

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

基于时间着色Petri网的SIP协议验证与分析

随着SIP(Session Initiation Protocol)被3G通信选择为下一代移动网络的会话控制机制,保证SIP协议设计和实现无缺陷、运行稳定可靠成为SIP协议应用过程中亟需研究和解决的关键问题。充分利用时间着色Petri网(Timed Colored Petri Nets,TCPN)在描述和分析具有复杂交互行为及时间约束的系统方面的优势,给出了SIP协议的层次TCPN模型,并集成多种模型分析技术,完成SIP协议设计的正确性验证;同时通过正则表达式完成协议模型的生成路径分析,指出其中存在的死锁状态并分析原因。提出了相应的协议设计改进方案,验证了设计方案的正确性,从而有效增强了SIP协议在实际应用中的可行性和可靠性。

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

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

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

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