A Method of Composing Communication Protocols with Priority Service

Masahiro HIGUCHI  Hiroyuki SEKI  Tadao KASAMI  

IEICE TRANSACTIONS on Communications   Vol.E75-B   No.10   pp.1032-1042
Publication Date: 1992/10/25
Online ISSN: 
Print ISSN: 0916-8516
Type of Manuscript: Special Section PAPER (Special Issue on Communication Software Technologies)
communication protocol,  communicating sequential machines,  safety property,  verification,  reachability analysis,  

Full Text: PDF(878.3KB)>>
Buy this Article

Many practical communication protocols provide priority service as well as ordinary service. In such a protocol, the protocol machines can initiate a priority service at most of the states. This characteristic leads an extreme increment of the number of state transitions on the protocol machines and causes state space explosion in verification of safety property of the protocol. This paper describes a method of constructing a communication protocol from composition of a subprotocol for ordinary service and that for priority service. This paper also presents a sufficient condition for a composed protocol to inherit safety property from the subprotocols. By using the composition method and the sufficient condition, the decision problem for safety property of the composed protocol can be reduced to those of the subprotocols. An experimental result of verification of a part of OSI session protocol is also described. The result shows that the method can reduce the computation time for verifying safety property to about 3% against the naive way.