An Estelle translator for incremental protocol verification

Chung Ming Huang, Jenq Muh Hsu

Research output: Contribution to journalArticle

Abstract

Formal Description Techniques (FDTs) provide formal support for each phase of protocol development. Estelle is one of the FDTs proposed by the International Organization for Standardization (ISO) to formally specify distributed systems, especially for communication protocols. In this paper, we present the development of an Estelle translator which allows protocol designers to interactively add/delete transitions at the run time of protocol verification. The Estelle translator can translate Estelle-specified protocols into the internal extended finite state machine tables, which have corresponding information of each protocol entity. The main feature of the Estelle translator is its capacity to support incremental protocol verification. The incremental translating components in our Estelle translator allow protocol designers to modify protocols at the run time and continue the verification at the modification point incrementally. That is, our Estelle translator allows protocol designers interactively modifying Estelle-specified protocols in order to eliminate logical errors at the run time, interpret the modified part, and then continue verification incrementally at the modification point. In this way, protocol designers can design Estelle-specified protocols interactively and incrementally using our translator.

Original languageEnglish
Pages (from-to)179-192
Number of pages14
JournalJournal of the Chinese Institute of Engineers, Transactions of the Chinese Institute of Engineers,Series A/Chung-kuo Kung Ch'eng Hsuch K'an
Volume19
Issue number2
DOIs
Publication statusPublished - 1996 Jan 1

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Fingerprint Dive into the research topics of 'An Estelle translator for incremental protocol verification'. Together they form a unique fingerprint.

  • Cite this