TCP协议的Z语言描述

Formal Description of Transmission Control Protocol

计算机通信协议的开发难度随着复杂程度的增加而日益增大,潜在错误也越来越多,其中对协议规格说明理解的偏差是重要原因之一.因此需要对规格说明进行验证和确认,并对协议的实现进行一致性测试.一致性测试就是测试协议的实现是否与相关国际标准中的规格说明相一致.协议的规格说明主要是以自然语言描述的,对其进行形式化是为了精确描述协议,因而可减少这类错误的出现.Z语言是基于一阶谓词逻辑和集合论的形式规格说明语言,采用了严格的数学理论,可产生简明、精确、无歧义且可证明的规格说明.本文以TCP协议为例详细介绍了如何使用Z语言对协议进行形式化,为协议一致性测试打下基础.

The degree of difficulty in developing computer communication protocols grows with their complexities, so do the potential mistakes. One of the main reasons is misunderstanding of the specifications. Therefore, one should verify and validate the specifications and test the conformance of protocols. The conformance test of protocol is to test the conformance between implementation of protocols and their specifications in accordance with international standards. Specifications of protocols are mainly described in natural languages, and the aim of their formalization is to describe them accurately so that one can reduce the occurrence of mistakes. Z is a formal specification language based on the first order predicate logic and set theory. It can generate concise, accurate and conformable specifications. This paper introduces a method of protocol formalization with Z in detail, using transmission control protocol (TCP) as an example, and provides a basis for the conformance test of protocols.