Protocol Verification Algorithm Using Reduced Reachability Analysis

Masaki ITOH; Haruhisa ICHIKAWA

Protocol Verification Algorithm Using Reduced Reachability Analysis

Masaki ITOH, Haruhisa ICHIKAWA

Full Text Views

0

Share
Cite this

Summary :

An extended state transition model and verification algorithm are proposed for specification and verification of protocols. The state transition model is an extention of Zafiropulo's two process protocol model to specify protocols designed for communication between more than two processes. A concept of Reduced Implementation Sequence (RIS)" is introduced to establish a protocol verification algorithm. By using RIS, potential movements of modeled systems are compactly described and the computation time necessary for verification becomes much shorter than that required for the method based on the traditional reachability analysis.

Publication: IEICE TRANSACTIONS on transactions Vol.E66-E No.2 pp.88-93

Publication Date: 1983/02/25

Publicized

Online ISSN

DOI

Type of Manuscript: PAPER

Category: Protocol

Authors

Masaki ITOH
Haruhisa ICHIKAWA

Keyword

Cite this

Copy

Masaki ITOH, Haruhisa ICHIKAWA, "Protocol Verification Algorithm Using Reduced Reachability Analysis" in IEICE TRANSACTIONS on transactions, vol. E66-E, no. 2, pp. 88-93, February 1983, doi: .
Abstract: An extended state transition model and verification algorithm are proposed for specification and verification of protocols. The state transition model is an extention of Zafiropulo's two process protocol model to specify protocols designed for communication between more than two processes. A concept of Reduced Implementation Sequence (RIS)" is introduced to establish a protocol verification algorithm. By using RIS, potential movements of modeled systems are compactly described and the computation time necessary for verification becomes much shorter than that required for the method based on the traditional reachability analysis.
URL: https://globals.ieice.org/en_transactions/transactions/10.1587/e66-e_2_88/_p

Copy

@ARTICLE{e66-e_2_88,
author={Masaki ITOH, Haruhisa ICHIKAWA, },
journal={IEICE TRANSACTIONS on transactions},
title={Protocol Verification Algorithm Using Reduced Reachability Analysis},
year={1983},
volume={E66-E},
number={2},
pages={88-93},
abstract={An extended state transition model and verification algorithm are proposed for specification and verification of protocols. The state transition model is an extention of Zafiropulo's two process protocol model to specify protocols designed for communication between more than two processes. A concept of Reduced Implementation Sequence (RIS)" is introduced to establish a protocol verification algorithm. By using RIS, potential movements of modeled systems are compactly described and the computation time necessary for verification becomes much shorter than that required for the method based on the traditional reachability analysis.},
keywords={},
doi={},
ISSN={},
month={February},}

Copy

TY - JOUR
TI - Protocol Verification Algorithm Using Reduced Reachability Analysis
T2 - IEICE TRANSACTIONS on transactions
SP - 88
EP - 93
AU - Masaki ITOH
AU - Haruhisa ICHIKAWA
PY - 1983
DO -
JO - IEICE TRANSACTIONS on transactions
SN -
VL - E66-E
IS - 2
JA - IEICE TRANSACTIONS on transactions
Y1 - February 1983
AB - An extended state transition model and verification algorithm are proposed for specification and verification of protocols. The state transition model is an extention of Zafiropulo's two process protocol model to specify protocols designed for communication between more than two processes. A concept of Reduced Implementation Sequence (RIS)" is introduced to establish a protocol verification algorithm. By using RIS, potential movements of modeled systems are compactly described and the computation time necessary for verification becomes much shorter than that required for the method based on the traditional reachability analysis.
ER -