A multi-event-one-transition plus incremental processing protocol verification method

Chung-Ming Huang, Huei Yang Lai, Duen Tay Huang

Research output: Contribution to journalArticle

Abstract

Formal Description Techniques (FDTs), e.g. ISO's Estelle and CCITT's SDL, are becoming the standard mechanisms for specifying communication protocols. New protocol verification techniques, e.g., global state reduction techniques for FDT-based global state reachability analysis, are therefore required to verify FDT-specified protocols. Most of the currently existing global state reduction techniques are based on the Communicating Finite State Machine (CFSM) model. Therefore, these reduction techniques cannot be directly applied to ISO's Estelle or CCITT's SDL, which are Extended CFSM (ECFSM)-based Formal Description Techniques (FDTs), protocol verification systems. By modifying Itoh and Ichikawa's CFSM-based reduction technique to be ECFSM-based, by modifying Huang et al.'s CFSM-based incremental verification technique to be ECFSM-based, and by incorporating Chu and Liu's ECFSM-based reduction technique, i.e., dead and live variable analysis, this paper proposes a Multi-event-one-transition Plus Incremental processing (MPI) protocol verification technique for verification of ECFSM-based n-entity protocols. In this way, the MPI verification technique can be directly applied to Estelle or SDL protocol verification systems.

Original languageEnglish
Pages (from-to)215-241
Number of pages27
JournalJournal of Information Science and Engineering
Volume12
Issue number2
Publication statusPublished - 1996 Jun 1

Fingerprint

Network protocols
Finite automata
event
Processing
communication

All Science Journal Classification (ASJC) codes

  • Software
  • Human-Computer Interaction
  • Hardware and Architecture
  • Library and Information Sciences
  • Computational Theory and Mathematics

Cite this

@article{f0f1c54a7f4d43dd97b7752810f2bbb3,
title = "A multi-event-one-transition plus incremental processing protocol verification method",
abstract = "Formal Description Techniques (FDTs), e.g. ISO's Estelle and CCITT's SDL, are becoming the standard mechanisms for specifying communication protocols. New protocol verification techniques, e.g., global state reduction techniques for FDT-based global state reachability analysis, are therefore required to verify FDT-specified protocols. Most of the currently existing global state reduction techniques are based on the Communicating Finite State Machine (CFSM) model. Therefore, these reduction techniques cannot be directly applied to ISO's Estelle or CCITT's SDL, which are Extended CFSM (ECFSM)-based Formal Description Techniques (FDTs), protocol verification systems. By modifying Itoh and Ichikawa's CFSM-based reduction technique to be ECFSM-based, by modifying Huang et al.'s CFSM-based incremental verification technique to be ECFSM-based, and by incorporating Chu and Liu's ECFSM-based reduction technique, i.e., dead and live variable analysis, this paper proposes a Multi-event-one-transition Plus Incremental processing (MPI) protocol verification technique for verification of ECFSM-based n-entity protocols. In this way, the MPI verification technique can be directly applied to Estelle or SDL protocol verification systems.",
author = "Chung-Ming Huang and Lai, {Huei Yang} and Huang, {Duen Tay}",
year = "1996",
month = "6",
day = "1",
language = "English",
volume = "12",
pages = "215--241",
journal = "Journal of Information Science and Engineering",
issn = "1016-2364",
publisher = "Institute of Information Science",
number = "2",

}

A multi-event-one-transition plus incremental processing protocol verification method. / Huang, Chung-Ming; Lai, Huei Yang; Huang, Duen Tay.

In: Journal of Information Science and Engineering, Vol. 12, No. 2, 01.06.1996, p. 215-241.

Research output: Contribution to journalArticle

TY - JOUR

T1 - A multi-event-one-transition plus incremental processing protocol verification method

AU - Huang, Chung-Ming

AU - Lai, Huei Yang

AU - Huang, Duen Tay

PY - 1996/6/1

Y1 - 1996/6/1

N2 - Formal Description Techniques (FDTs), e.g. ISO's Estelle and CCITT's SDL, are becoming the standard mechanisms for specifying communication protocols. New protocol verification techniques, e.g., global state reduction techniques for FDT-based global state reachability analysis, are therefore required to verify FDT-specified protocols. Most of the currently existing global state reduction techniques are based on the Communicating Finite State Machine (CFSM) model. Therefore, these reduction techniques cannot be directly applied to ISO's Estelle or CCITT's SDL, which are Extended CFSM (ECFSM)-based Formal Description Techniques (FDTs), protocol verification systems. By modifying Itoh and Ichikawa's CFSM-based reduction technique to be ECFSM-based, by modifying Huang et al.'s CFSM-based incremental verification technique to be ECFSM-based, and by incorporating Chu and Liu's ECFSM-based reduction technique, i.e., dead and live variable analysis, this paper proposes a Multi-event-one-transition Plus Incremental processing (MPI) protocol verification technique for verification of ECFSM-based n-entity protocols. In this way, the MPI verification technique can be directly applied to Estelle or SDL protocol verification systems.

AB - Formal Description Techniques (FDTs), e.g. ISO's Estelle and CCITT's SDL, are becoming the standard mechanisms for specifying communication protocols. New protocol verification techniques, e.g., global state reduction techniques for FDT-based global state reachability analysis, are therefore required to verify FDT-specified protocols. Most of the currently existing global state reduction techniques are based on the Communicating Finite State Machine (CFSM) model. Therefore, these reduction techniques cannot be directly applied to ISO's Estelle or CCITT's SDL, which are Extended CFSM (ECFSM)-based Formal Description Techniques (FDTs), protocol verification systems. By modifying Itoh and Ichikawa's CFSM-based reduction technique to be ECFSM-based, by modifying Huang et al.'s CFSM-based incremental verification technique to be ECFSM-based, and by incorporating Chu and Liu's ECFSM-based reduction technique, i.e., dead and live variable analysis, this paper proposes a Multi-event-one-transition Plus Incremental processing (MPI) protocol verification technique for verification of ECFSM-based n-entity protocols. In this way, the MPI verification technique can be directly applied to Estelle or SDL protocol verification systems.

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

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

M3 - Article

VL - 12

SP - 215

EP - 241

JO - Journal of Information Science and Engineering

JF - Journal of Information Science and Engineering

SN - 1016-2364

IS - 2

ER -