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 Verification Method via Invariant for Communication Protocols Modeled as Extended Communicating Finite-State Machines
Masahiro HIGUCHI Osamu SHIRAKAWA Hiroyuki SEKI Mamoru FUJII Tadao KASAMI
IEICE TRANSACTIONS on Communications
Publication Date: 1993/11/25
Print ISSN: 0916-8516
Type of Manuscript: PAPER
Category: Signaling System and Communication Protocol
integral register, unbounded communication channel, safety property, term rewriting system, OSI session protocol,
Full Text: PDF(892KB)>>
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.