A Verification Method via Invariant for Communication Protocols Modeled as Extended Communicating Finite-State Machines
Summary :
This paper presents a method for verifying safety property of a communication protocol modeled as two extended communicating finite-state machines with two unbounded FIFO channels connecting them. In this method, four types of atomic formulae specifying a condition on a machine and a condition on a sequence of messages in a channel are introduced. A human verifier describes a logical formula which expresses conditions expected to be satisfied by all reachable global states, and a verification system proves that the formula is indeed satisfied by such states (i.e. the formula is an invariant) by induction. If the invariant is never satisfied in any unsafe state, it can be concluded that the protocol it safe. To show the effectiveness of this method, a sample protocol extracted from the data transfer phase of the OSI session protocol was verified by using the verification system.
- Publication
- IEICE TRANSACTIONS on Communications Vol.E76-B No.11 pp.1363-1372
- Publication Date
- 1993/11/25
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- PAPER
- Category
- Signaling System and Communication Protocol
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Masahiro HIGUCHI, Osamu SHIRAKAWA, Hiroyuki SEKI, Mamoru FUJII, Tadao KASAMI, "A Verification Method via Invariant for Communication Protocols Modeled as Extended Communicating Finite-State Machines" in IEICE TRANSACTIONS on Communications,
vol. E76-B, no. 11, pp. 1363-1372, November 1993, doi: .
Abstract: This paper presents a method for verifying safety property of a communication protocol modeled as two extended communicating finite-state machines with two unbounded FIFO channels connecting them. In this method, four types of atomic formulae specifying a condition on a machine and a condition on a sequence of messages in a channel are introduced. A human verifier describes a logical formula which expresses conditions expected to be satisfied by all reachable global states, and a verification system proves that the formula is indeed satisfied by such states (i.e. the formula is an invariant) by induction. If the invariant is never satisfied in any unsafe state, it can be concluded that the protocol it safe. To show the effectiveness of this method, a sample protocol extracted from the data transfer phase of the OSI session protocol was verified by using the verification system.
URL: https://global.ieice.org/en_transactions/communications/10.1587/e76-b_11_1363/_p
Copy
@ARTICLE{e76-b_11_1363,
author={Masahiro HIGUCHI, Osamu SHIRAKAWA, Hiroyuki SEKI, Mamoru FUJII, Tadao KASAMI, },
journal={IEICE TRANSACTIONS on Communications},
title={A Verification Method via Invariant for Communication Protocols Modeled as Extended Communicating Finite-State Machines},
year={1993},
volume={E76-B},
number={11},
pages={1363-1372},
abstract={This paper presents a method for verifying safety property of a communication protocol modeled as two extended communicating finite-state machines with two unbounded FIFO channels connecting them. In this method, four types of atomic formulae specifying a condition on a machine and a condition on a sequence of messages in a channel are introduced. A human verifier describes a logical formula which expresses conditions expected to be satisfied by all reachable global states, and a verification system proves that the formula is indeed satisfied by such states (i.e. the formula is an invariant) by induction. If the invariant is never satisfied in any unsafe state, it can be concluded that the protocol it safe. To show the effectiveness of this method, a sample protocol extracted from the data transfer phase of the OSI session protocol was verified by using the verification system.},
keywords={},
doi={},
ISSN={},
month={November},}
Copy
TY - JOUR
TI - A Verification Method via Invariant for Communication Protocols Modeled as Extended Communicating Finite-State Machines
T2 - IEICE TRANSACTIONS on Communications
SP - 1363
EP - 1372
AU - Masahiro HIGUCHI
AU - Osamu SHIRAKAWA
AU - Hiroyuki SEKI
AU - Mamoru FUJII
AU - Tadao KASAMI
PY - 1993
DO -
JO - IEICE TRANSACTIONS on Communications
SN -
VL - E76-B
IS - 11
JA - IEICE TRANSACTIONS on Communications
Y1 - November 1993
AB - This paper presents a method for verifying safety property of a communication protocol modeled as two extended communicating finite-state machines with two unbounded FIFO channels connecting them. In this method, four types of atomic formulae specifying a condition on a machine and a condition on a sequence of messages in a channel are introduced. A human verifier describes a logical formula which expresses conditions expected to be satisfied by all reachable global states, and a verification system proves that the formula is indeed satisfied by such states (i.e. the formula is an invariant) by induction. If the invariant is never satisfied in any unsafe state, it can be concluded that the protocol it safe. To show the effectiveness of this method, a sample protocol extracted from the data transfer phase of the OSI session protocol was verified by using the verification system.
ER -
English
