Incremental maximal progress protocol verification for ECFSM-based protocols

Chung-Ming Huang, Jenq Muh Hsu

Research output: Contribution to journalArticle

Abstract

Protocol verification is an activity involving detection of logical errors in communication protocols. In this paper, we propose an integrated approach to protocol verification. We modify the Communicating Finite State Machine (CFSM)-based maximal progress state reduction technique so that it is Extended Communicating Finite State Machine (ECFSM)-based. Next, we propose an ECFSM-based incremental protocol verification technique based on the maximal progress principle. To further reduce the number of global states to be explored, the dead and live variables concept is incorporated. As a result, an incremental maximal progress protocol verification method is derived based on the integration approach. Our ECFSM-based method is, therefore, applicable to the ECFSM-based Formal Description Techniques (FDTs), e.g., the International Standard Organization's (ISO) Estelle or International Telegraph and Telephone Consultative Committee's (CCITT) Specification and Description Language (SDL). Based on the incremental maximal progress verification method, an Estelle-based Incremental Maximal progress Protocol Verification System (EIMPVS) is developed on SUN SPARC workstations. In this way, protocol designers can use our EIMPVS to verify Estelle-specified protocols.

Original languageEnglish
Pages (from-to)600-615
Number of pages16
JournalProceedings of the National Science Council, Republic of China, Part A: Physical Science and Engineering
Volume22
Issue number5
Publication statusPublished - 1998 Sep

Fingerprint

Finite automata
Network protocols
Computer systems
Telegraph
Specification languages
Computer workstations
Telephone

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Cite this

@article{7297d41dc94f4c8086903e1dcb341713,
title = "Incremental maximal progress protocol verification for ECFSM-based protocols",
abstract = "Protocol verification is an activity involving detection of logical errors in communication protocols. In this paper, we propose an integrated approach to protocol verification. We modify the Communicating Finite State Machine (CFSM)-based maximal progress state reduction technique so that it is Extended Communicating Finite State Machine (ECFSM)-based. Next, we propose an ECFSM-based incremental protocol verification technique based on the maximal progress principle. To further reduce the number of global states to be explored, the dead and live variables concept is incorporated. As a result, an incremental maximal progress protocol verification method is derived based on the integration approach. Our ECFSM-based method is, therefore, applicable to the ECFSM-based Formal Description Techniques (FDTs), e.g., the International Standard Organization's (ISO) Estelle or International Telegraph and Telephone Consultative Committee's (CCITT) Specification and Description Language (SDL). Based on the incremental maximal progress verification method, an Estelle-based Incremental Maximal progress Protocol Verification System (EIMPVS) is developed on SUN SPARC workstations. In this way, protocol designers can use our EIMPVS to verify Estelle-specified protocols.",
author = "Chung-Ming Huang and Hsu, {Jenq Muh}",
year = "1998",
month = "9",
language = "English",
volume = "22",
pages = "600--615",
journal = "Proceedings of the National Science Council, Republic of China, Part A: Physical Science and Engineering",
issn = "0255-6588",
publisher = "National Science Council",
number = "5",

}

TY - JOUR

T1 - Incremental maximal progress protocol verification for ECFSM-based protocols

AU - Huang, Chung-Ming

AU - Hsu, Jenq Muh

PY - 1998/9

Y1 - 1998/9

N2 - Protocol verification is an activity involving detection of logical errors in communication protocols. In this paper, we propose an integrated approach to protocol verification. We modify the Communicating Finite State Machine (CFSM)-based maximal progress state reduction technique so that it is Extended Communicating Finite State Machine (ECFSM)-based. Next, we propose an ECFSM-based incremental protocol verification technique based on the maximal progress principle. To further reduce the number of global states to be explored, the dead and live variables concept is incorporated. As a result, an incremental maximal progress protocol verification method is derived based on the integration approach. Our ECFSM-based method is, therefore, applicable to the ECFSM-based Formal Description Techniques (FDTs), e.g., the International Standard Organization's (ISO) Estelle or International Telegraph and Telephone Consultative Committee's (CCITT) Specification and Description Language (SDL). Based on the incremental maximal progress verification method, an Estelle-based Incremental Maximal progress Protocol Verification System (EIMPVS) is developed on SUN SPARC workstations. In this way, protocol designers can use our EIMPVS to verify Estelle-specified protocols.

AB - Protocol verification is an activity involving detection of logical errors in communication protocols. In this paper, we propose an integrated approach to protocol verification. We modify the Communicating Finite State Machine (CFSM)-based maximal progress state reduction technique so that it is Extended Communicating Finite State Machine (ECFSM)-based. Next, we propose an ECFSM-based incremental protocol verification technique based on the maximal progress principle. To further reduce the number of global states to be explored, the dead and live variables concept is incorporated. As a result, an incremental maximal progress protocol verification method is derived based on the integration approach. Our ECFSM-based method is, therefore, applicable to the ECFSM-based Formal Description Techniques (FDTs), e.g., the International Standard Organization's (ISO) Estelle or International Telegraph and Telephone Consultative Committee's (CCITT) Specification and Description Language (SDL). Based on the incremental maximal progress verification method, an Estelle-based Incremental Maximal progress Protocol Verification System (EIMPVS) is developed on SUN SPARC workstations. In this way, protocol designers can use our EIMPVS to verify Estelle-specified protocols.

UR - http://www.scopus.com/inward/record.url?scp=0032166878&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0032166878&partnerID=8YFLogxK

M3 - Article

VL - 22

SP - 600

EP - 615

JO - Proceedings of the National Science Council, Republic of China, Part A: Physical Science and Engineering

JF - Proceedings of the National Science Council, Republic of China, Part A: Physical Science and Engineering

SN - 0255-6588

IS - 5

ER -