论文部分内容阅读
协议是计算机网络的命脉，协议复杂性的提高导致协议工程学科的出现。协议工程的主要活动包括协议描述、验证、性能分析、自动实现和一致性测试，其中协议描述和分析是整个协议工程中最重要的活动环节，是协议工程其它活动的基础。论文在总结比较现有的各种形式描述技术(FDT)的基础之上，重点论述了采用Petri网作为协议描述和分析工具的优势所在。为了更好的扩展时间Petri网的模拟能力以及建模的方便，在Merlin定义的时间Petri网的基础之上添加了抑止弧以实现对变迁激发的另一种控制，提出了带抑止弧的时间Petri网系统(ETPN)，并定义了ETPN网系统的状态、变迁激发的条件和变迁激发的规则。在对该网系统进行分析的基础之上，发展了传统的可达分析技术。应用带抑止弧的时间Petri网对IEEE802.2 LLC3型协议进行了建模。根据本文提出的可达分析技术，推导出了保证协议正确操作的参数间的时间关系，根据该时间关系，我们得到了所建模型的简化的可达标识图，并对该模型的动态特性进行了初步分析。