一种兼顾协议正确性验证和性能评估的Petri网方法

摘要：

基于Petri网的协议形式化分析方法由于其精炼、简洁和无二义性逐步成为分析协议的一条可靠和准确的途径,但是协议的形式化分析目前研究还不够深入,协议分析的两个重点内容正确性验证和性能评估所需要的模型不同,一种模型只能解决一方面的工作.为了有效地解决这一问题,文中提出了一种用原型Petri网作为协议验证模型的思路和方法,在不改变原型Petri网结构的基础上对变迁赋予发生时延,解决了协议的性能评估问题.本文还给出了协议验证内容与Petri网分析方法的对应关系,并对0-1停止等待协议进行了详细的分析,最后把0-1停止等待协议的原型Petri网模型转化为时延petri网,对协议的性能进行了评估.

关键词：协议验证、形式化分析、时延Petri网、协议性能评估、0-1停止等待协议

所属期刊栏目：32

分类号：TP3(计算技术、计算机技术)

资助基金：中国科学院资助项目60173053

在线出版日期：2006-02-23（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：48-52