Parallel protocol verification: The two-phase algorithm and complexity analysis

Maria C. Yuang, A. Kershenbaum

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

Protocol verification detects the existence of logic errors in protocol design specifications. Various verification approaches have been proposed to deal with the state space explosion problem resulting from the reachability analysis. This paper proposes a parallel protocol verification algorithm, called the Two-Phase algorithm, in an attempt to provide a maximum of verification with a minimum of state space. This algorithm allows verification for all FSMs to be executed in parallel through exploring fewer states. To quantify the reduction in state space, the paper provides the state space complexity comparison between the reachability analysis and the Two-Phase algorithm. The paper defines four protocol models giving the lower and upper bound state space complexity according to both state and channel synchronization characteristics of protocols. For each model, the state space complexity of these two verification algorithms are analyzed and compared. The Two-Phase algorithm is shown to require much smaller state space. To support the analytical result, this paper also gives experimental results on several protocols, including the Call Set-Up and Termination phases of the CCITT X.25 and X.75 protocols.

Original languageEnglish
Title of host publicationAutomatic Verification Methods for Finite State Systems - International Workshop, Proceedings
EditorsJoseph Sifakis
PublisherSpringer Verlag
Pages303-316
Number of pages14
ISBN (Print)9783540521488
DOIs
StatePublished - 1 Jan 1990
Event1st International Workshop on Automatic Verification Methods for Finite State Systems, 1989 - Grenoble, France
Duration: 12 Jun 198914 Jun 1989

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume407 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference1st International Workshop on Automatic Verification Methods for Finite State Systems, 1989
CountryFrance
CityGrenoble
Period12/06/8914/06/89

Fingerprint Dive into the research topics of 'Parallel protocol verification: The two-phase algorithm and complexity analysis'. Together they form a unique fingerprint.

Cite this