摘要
基于Petri网的网络协议建模技术需要更有效地与现有通用网络协议仿真技术协同工作,结合CPN和IPN,提出了一种新的Petri网派生类CIPN用于网络协议的建模和形式化分析,突出了协议的离散事件系统特性。给出了CIPN的定义,并讨论了CIPN的运行机制,证明了CIPN事件可观测性的充要条件。通过一个MACA协议作为示例,完成了从网络协议的一般CPN模型到CIPN模型的等价性转换,并利用CIPN的事件可观测性定理对MACA协议进行了事件观测性分析。
The Petri net-based modeling technique for network protocols need cooperate with existing network protocol simulators more effectively. Combing CPN and IPN together, this paper introduced a novel descent of Petri net named CIPN in order to get a model highlighting the DES essence and take a formal analysis easily. Then discussed definition and operation mechanism of CIPN. Also the necessary and sufficient condition for event observability of CIPN got proofed. A MACA protocol-based example shows that the transmission from CPN model to its equative CIPN counterpart. And analyzed the event observability of MACA with employing event observability theorem in CIPN.
出处
《计算机应用研究》
CSCD
北大核心
2008年第11期3430-3433,共4页
Application Research of Computers
基金
电子信息产业发展基金资助项目(财建[2006]549号,信部运[2006]634号)
关键词
网络协议
离散事件系统
着色解释Petri网
协议工程
network protocols
discrete event system （DES）
colored interpreted Petri nets （CIPN）
protocol engineering
