An Estelle-based incremental protocol design system

Chung-Ming Huang, Jenq Muh Hsu, Huei Yang Lai, Duen Tay Huang, Jao Chiang Pong

Research output: Contribution to journalArticle

1 Citation (Scopus)

Abstract

Formal description techniques (FDTs) provide formal and abstract ways to specify what protocols have to do and what features protocols need. Estelle is an FDT defined by the International Organization for Standardization for protocol specifications. We present an incremental protocol design system that contains an incremental protocol verification technique and an Estelle translator. Our incremental protocol design system allows on-line reverification after respecification. That is, instead of verifying respecified (modified) protocols from scratch, the reverification procedure is executed continuously and incrementally at the modification point. Using the translator, Estelle protocol specifications can be translated and interpreted for protocol verification. To meet the requirement of modifying protocol specifications written in Estelle at run time, the Estelle translator allows incremental translation and interpretation of the modified Estelle specification part for incremental verification. To further reduce the number of global states to be explored, the concept of dead and live variables is incorporated into our incremental verification technique. Based on the incremental verification technique and the Estelle translator, an incremental protocol design system (IPDS) is developed on SUN SPARC OPENLOOK work-stations. Using IPDS, protocol designers can analyze the verification results, interactively modify the protocols, and then continue the verification incrementally.

Original languageEnglish
Pages (from-to)115-135
Number of pages21
JournalJournal of Systems and Software
Volume36
Issue number2
DOIs
Publication statusPublished - 1997 Jan 1

Fingerprint

Network protocols
Specifications
Online systems
Standardization
Computer systems

All Science Journal Classification (ASJC) codes

  • Software
  • Information Systems
  • Hardware and Architecture

Cite this

Huang, Chung-Ming ; Hsu, Jenq Muh ; Lai, Huei Yang ; Huang, Duen Tay ; Pong, Jao Chiang. / An Estelle-based incremental protocol design system. In: Journal of Systems and Software. 1997 ; Vol. 36, No. 2. pp. 115-135.
@article{19d3a319815845668b3b6994e7ee9c8a,
title = "An Estelle-based incremental protocol design system",
abstract = "Formal description techniques (FDTs) provide formal and abstract ways to specify what protocols have to do and what features protocols need. Estelle is an FDT defined by the International Organization for Standardization for protocol specifications. We present an incremental protocol design system that contains an incremental protocol verification technique and an Estelle translator. Our incremental protocol design system allows on-line reverification after respecification. That is, instead of verifying respecified (modified) protocols from scratch, the reverification procedure is executed continuously and incrementally at the modification point. Using the translator, Estelle protocol specifications can be translated and interpreted for protocol verification. To meet the requirement of modifying protocol specifications written in Estelle at run time, the Estelle translator allows incremental translation and interpretation of the modified Estelle specification part for incremental verification. To further reduce the number of global states to be explored, the concept of dead and live variables is incorporated into our incremental verification technique. Based on the incremental verification technique and the Estelle translator, an incremental protocol design system (IPDS) is developed on SUN SPARC OPENLOOK work-stations. Using IPDS, protocol designers can analyze the verification results, interactively modify the protocols, and then continue the verification incrementally.",
author = "Chung-Ming Huang and Hsu, {Jenq Muh} and Lai, {Huei Yang} and Huang, {Duen Tay} and Pong, {Jao Chiang}",
year = "1997",
month = "1",
day = "1",
doi = "10.1016/0164-1212(95)00065-8",
language = "English",
volume = "36",
pages = "115--135",
journal = "Journal of Systems and Software",
issn = "0164-1212",
publisher = "Elsevier Inc.",
number = "2",

}

An Estelle-based incremental protocol design system. / Huang, Chung-Ming; Hsu, Jenq Muh; Lai, Huei Yang; Huang, Duen Tay; Pong, Jao Chiang.

In: Journal of Systems and Software, Vol. 36, No. 2, 01.01.1997, p. 115-135.

Research output: Contribution to journalArticle

TY - JOUR

T1 - An Estelle-based incremental protocol design system

AU - Huang, Chung-Ming

AU - Hsu, Jenq Muh

AU - Lai, Huei Yang

AU - Huang, Duen Tay

AU - Pong, Jao Chiang

PY - 1997/1/1

Y1 - 1997/1/1

N2 - Formal description techniques (FDTs) provide formal and abstract ways to specify what protocols have to do and what features protocols need. Estelle is an FDT defined by the International Organization for Standardization for protocol specifications. We present an incremental protocol design system that contains an incremental protocol verification technique and an Estelle translator. Our incremental protocol design system allows on-line reverification after respecification. That is, instead of verifying respecified (modified) protocols from scratch, the reverification procedure is executed continuously and incrementally at the modification point. Using the translator, Estelle protocol specifications can be translated and interpreted for protocol verification. To meet the requirement of modifying protocol specifications written in Estelle at run time, the Estelle translator allows incremental translation and interpretation of the modified Estelle specification part for incremental verification. To further reduce the number of global states to be explored, the concept of dead and live variables is incorporated into our incremental verification technique. Based on the incremental verification technique and the Estelle translator, an incremental protocol design system (IPDS) is developed on SUN SPARC OPENLOOK work-stations. Using IPDS, protocol designers can analyze the verification results, interactively modify the protocols, and then continue the verification incrementally.

AB - Formal description techniques (FDTs) provide formal and abstract ways to specify what protocols have to do and what features protocols need. Estelle is an FDT defined by the International Organization for Standardization for protocol specifications. We present an incremental protocol design system that contains an incremental protocol verification technique and an Estelle translator. Our incremental protocol design system allows on-line reverification after respecification. That is, instead of verifying respecified (modified) protocols from scratch, the reverification procedure is executed continuously and incrementally at the modification point. Using the translator, Estelle protocol specifications can be translated and interpreted for protocol verification. To meet the requirement of modifying protocol specifications written in Estelle at run time, the Estelle translator allows incremental translation and interpretation of the modified Estelle specification part for incremental verification. To further reduce the number of global states to be explored, the concept of dead and live variables is incorporated into our incremental verification technique. Based on the incremental verification technique and the Estelle translator, an incremental protocol design system (IPDS) is developed on SUN SPARC OPENLOOK work-stations. Using IPDS, protocol designers can analyze the verification results, interactively modify the protocols, and then continue the verification incrementally.

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

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

U2 - 10.1016/0164-1212(95)00065-8

DO - 10.1016/0164-1212(95)00065-8

M3 - Article

VL - 36

SP - 115

EP - 135

JO - Journal of Systems and Software

JF - Journal of Systems and Software

SN - 0164-1212

IS - 2

ER -