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

Protocol Validation and Performance Evaluates Based on Petri Nets

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

Formal methods for the analysis of protocol based on Petri nets have been looked on a credible and exact way in protocol analysis. But now, the research on formal analysis of protocol is not thorough. Particularly, there is some conflict between protocol validation and evaluates. In this paper, we make a summary of the methods on protocol analysis based on Petri nets. Then we investigate the relationship between the protocol behavior and the properties of Petri nets. The most important is that we propose a new method about protocol analysis. This method gives a detail validation of protocol using prototype Petri net. We change prototype Petri net into Timed Petri net, so the protocol performance evaluates problem can be solved. As an example, we makea detail analysis of 0-1 stop-anawait protocol using Petri nets model and give evaluates the performance of it using TPN.