Timed protocol verification for Estelle-specified protocols

Chung Ming Huang, Shiun Wei Lee

研究成果: Article同行評審

3 引文 斯高帕斯(Scopus)


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.

頁(從 - 到)4-32
期刊Computer Communication Review
出版狀態Published - 1995

All Science Journal Classification (ASJC) codes

  • 軟體
  • 電腦網路與通信


深入研究「Timed protocol verification for Estelle-specified protocols」主題。共同形成了獨特的指紋。