Timed protocol verification for Estelle-specified protocols

Chung-Ming Huang, Shiun Wei Lee

Research output: Contribution to journalArticle

3 Citations (Scopus)

Abstract

This paper presents a new model, which is named Timed Communicating State Machine (TCSM), for specifying protocols that incorporate timed properties as part of their specifications. The TCSM model is similar to the Extended Communicating Finite State Machine (ECFSM) model. The major extension is providing an additional mechanism, i.e., a time interval attribute, for describing the timed properties. We also propose the corresponding formal TCSM-based timed verification scheme, i.e., a new timed global state reachability analysis. In the new timed global state reachability analysis, the exploration is decided by the predicate, the time relationships, and/or the input event. Using the TCSM model and the timed verification scheme, an Estelle-based Timed Protocol Verification System (ETPVS) has been developed on SUN SPARC workstations. In this way, timed protocols can be formally specified in Estelle and can also be verified using ETPVS.

Original languageEnglish
Pages (from-to)4-32
Number of pages29
JournalComputer Communication Review
Volume25
Issue number3
DOIs
Publication statusPublished - 1995 Jan 1

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Networks and Communications

Fingerprint Dive into the research topics of 'Timed protocol verification for Estelle-specified protocols'. Together they form a unique fingerprint.

  • Cite this