An Acyclic Expansion-Based Protocol Verification for Communications Software

Hironori SAITO  Yoshiaki KAKUDA  Toru HASEGAWA  Tohru KIKUNO  

Publication
IEICE TRANSACTIONS on Communications   Vol.E75-B   No.10   pp.998-1007
Publication Date: 1992/10/25
Online ISSN: 
DOI: 
Print ISSN: 0916-8516
Type of Manuscript: Special Section PAPER (Special Issue on Communication Software Technologies)
Category: 
Keyword: 
communications software,  communication protocol,  protocol verification,  finite state machine,  acyclic expansion algorithm,  temporal logic,  

Full Text: PDF(905.4KB)>>
Buy this Article




Summary: 
This paper presents a protocol verification method which verifies that the behaviors of a protocol meet requirements. In this method, a protocol specification is expressed as Extended Finite State Machines (EFSM's) that can handle variables, and requirements are expressed using a branching-time temporal logic for a concise and unambiguous description. Using the acyclic expansion algorithm extended such that it can deal with EFSM's, the verification method first generates a state transition graph consisting of executable transitions for each process. Then a branching-time temporal logic formula representing a requirement is evaluated on one of the generated graphs which is relevant to the requirement. An executable state transition graph for each process is much smaller than a global state transition graph which has been used in the conventional verification techniques to represent the behaviors of the whole protocol system consisting of all processes. The computation for generating the graphs is also reduced to much extent for a large complex protocol. As a result, the presented method achieves efficient verification for requirements regarding a state of a process, transmission and reception of messages by a process, varibales of a process and sequences that interact among processes. The validity of the method is illustrated in the paper by the verification of a path-updating protocol for requirements such as process state reachability or fair termination among processes.