A Method of Composing Communication Protocols with Priority Service

Masahiro HIGUCHI; Hiroyuki SEKI; Tadao KASAMI

A Method of Composing Communication Protocols with Priority Service

Masahiro HIGUCHI, Hiroyuki SEKI, Tadao KASAMI

Full Text Views

0

Share
Cite this

Summary :

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.

Publication: IEICE TRANSACTIONS on Communications Vol.E75-B No.10 pp.1032-1042

Publication Date: 1992/10/25

Publicized

Online ISSN

DOI

Type of Manuscript: Special Section PAPER (Special Issue on Communication Software Technologies)

Category

Cite this

Copy

Masahiro HIGUCHI, Hiroyuki SEKI, Tadao KASAMI, "A Method of Composing Communication Protocols with Priority Service" in IEICE TRANSACTIONS on Communications, vol. E75-B, no. 10, pp. 1032-1042, October 1992, doi: .
Abstract: 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.
URL: https://globals.ieice.org/en_transactions/communications/10.1587/e75-b_10_1032/_p

Copy

@ARTICLE{e75-b_10_1032,
author={Masahiro HIGUCHI, Hiroyuki SEKI, Tadao KASAMI, },
journal={IEICE TRANSACTIONS on Communications},
title={A Method of Composing Communication Protocols with Priority Service},
year={1992},
volume={E75-B},
number={10},
pages={1032-1042},
abstract={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.},
keywords={},
doi={},
ISSN={},
month={October},}

Copy

TY - JOUR
TI - A Method of Composing Communication Protocols with Priority Service
T2 - IEICE TRANSACTIONS on Communications
SP - 1032
EP - 1042
AU - Masahiro HIGUCHI
AU - Hiroyuki SEKI
AU - Tadao KASAMI
PY - 1992
DO -
JO - IEICE TRANSACTIONS on Communications
SN -
VL - E75-B
IS - 10
JA - IEICE TRANSACTIONS on Communications
Y1 - October 1992
AB - 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.
ER -