For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
A Method of Composing Communication Protocols with Priority Service
Masahiro HIGUCHI Hiroyuki SEKI Tadao KASAMI
IEICE TRANSACTIONS on Communications
Publication Date: 1992/10/25
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>>
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.