A Study of Formal Description and Product Validation Method for Communication Protocols

协议是计算机和终端之间通信的预定规则的集合。为了保持计算机网络的稳定运行，必须建立一个通信协议，并确认网络中使用的所有组件都符合所建立的协议。为此，应该对所有要连接到网络的产品进行协议验证。这被称为协议产品验证。协议有一个问题。产品验证是如何描述协议，以及如何生成用于协议验证的测试序列。通常协议本身是用自然语言描述的，这种描述不适合产品验证。在我们的研究中，提出了一种称为事件序列表达式的形式化协议描述语言，作为一种非常适合从自然语言表达式转换的表达式。设计了一个事件序列描述到状态转移表的转换系统。一旦获得状态转移表，就可以通过研究人员研究的方法生成用于产品验证的测试序列。该方法已在各种协议上进行了测试，包括HDLC和ISO标准传输层协议。通过实际应用证明了该方法的有效性。此外，还研究了从LOTOS到ESTELLE的转换系统。这种转换几乎相当于从事件序列表达式到状态转换表表达式的转换。发现LOTOS需要一些额外的信息才能完成转换。

Frotocol is a collection of predetermined rule for communication amoung computers and terminals. To maintain stable operation of a computer network, it is essential to establish a communication protocol and to confirm that all the components used in the network conform to the established protocol. For this purpose protocol validation should be made on all the products which is to be connected to the network. This is called protocol product validation.One problem for protocol. product validation is how to describe the protocol, and how to qenerate the test sequence to be used for protocol validation. Conventionaly protocol itself is described in natural language, and the description is not suited for product validation.In our study, a formal protocol description language called event sequence expression has been proposed as a expression well suited for conversion from natural language expression. We devised a conversion system of event sequence description to state transition table. Once state transition table is obtained, generation of test sequence for product valuidation is possible by a method studied by the researchers.The method has been tested on various protocols including HDLC and the ISO standard transport layer protocol. The usefulness of the approach has been proved through the applications. In addition, conversion system from LOTOS to ESTELLE has also been studied. The conversion almost corresponds to the conversion from event sequence expression to state transition tawble expression. Some additional information was found to be needed to LOTOS for complete conversion.