彭 勃



计算机网络通信协议验证技术的研究

彭 勃

北京联海信息系统有限公司，北京 100053

协议设计、开发的复杂性的增加，导致了协议工程技术的出现。针对协议工程活动中的协议验证与分析阶段，阐述了验证技术的目的与方法，分析了当今常用的协议模型技术，重点介绍了基于Petri网、FMS，以及时序逻辑TL模型的协议验证技术。

计算机网络；协议；协议工程；协议验证；Petri网

通信协议（communication protocol）是一组实体在执行某项任务中相互通信行为的规则和格式（语法和语义）[1]，它是数据通讯、计算机网络、多机系统等分布式系统的灵魂。随着网络与分布式系统的迅速发展，通信协议的形式化技术，其中包括一系列形式化理论、模型及实现方法已获得了长足的进步。所谓协议的形式化技术是指协议及服务规范的形式描述、设计验证、实现验证和一致性测试。在这些形式化技术中，形式描述与验证技术是整个协议设计与实现的基础，对协议实现的正确性、完全性和复杂度有至关重要的影响。

1 计算机网络协议的定义及特性

1.1 网络协议定义

网络协议是指在计算机与计算机之间进行通信必须遵循的一些事先约定好的规则。网络协议必须遵循标准化的体系结构，目前主要有ISO的标准和TCP/IP协议组标准，通信涉及的所有部分必须认同一套用于信息交换的规则。

1.2 网络协议特性

（1）活动性（liveness）：协议的活动性体现在终止性和进展性两方面，或者说，如果协议有终止性和进展性，它就具有活动性。……