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

All Science Journal Classification (ASJC) codes

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

Fingerprint Dive into the research topics of 'A multi-event-one-transition plus incremental processing protocol verification method'. Together they form a unique fingerprint.

  • Cite this