基于Petri网的高速网络协议的描述和验证

本项研究以协议描述、验证、合成、实现、性能分析和一致性测试等活动为环节的协议工程为目标，阐述基于谓词/变迁网系统的网络协议形式化描述和验证的基本理论，建立严格数学化的协议描述验证方法，开发协议分析和仿真运行的计算机辅助工具。本项研究所提出的EPr/TN网系统，是在剖析当前各种协议的基础上，结合Petri网异步并发特性克服节点爆炸问题，所建立的一项形式描术技术。这种形式技术具有描述能力强、抽象程度高、分析方便、直观形象和与协议系统接近等特点，EPr/TN网系统优于标准形式描述技术。本项理论成果和辅助工具，将积极推动高速网络协议的设计和开发，为协议软件的自动或半自动实现探索一条新的途径。