An Estelle interpreter for incremental protocol verification

Author

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

Author_Institution

Lab. of Comput.-Aided Protocol Eng., Nat. Cheng Kung Univ., Tainan, Taiwan

fYear

1993

fDate

19-22 Oct 1993

Firstpage

326

Lastpage

333

Abstract

Formal description techniques (FDTs) provide formal and abstract ways to specify what protocols have to do and what the features of the protocols need. Protocol verification is a process for detecting logical errors, such as deadlock, unspecified receptions, and channel overflow errors, in communication protocols. Estelle is a FDT defined by the International Organization for Standardization (ISO) for protocol specifications. The authors present an incremental protocol verification technique and an Estelle interpreter which accepts Estelle protocol specifications for incremental protocol verification

Keywords

formal specification; formal verification; program interpreters; protocols; specification languages; telecommunication computing; Estelle interpreter; Estelle protocol specifications; FDT; ISO; International Organization for Standardization; channel overflow errors; communication protocols; deadlock; formal description techniques; incremental protocol verification; protocol specifications; unspecified receptions; Automata; Communication system control; Councils; Explosions; ISO standards; Information processing; Protocols; Reachability analysis; Standardization; System recovery;

fLanguage

English

Publisher

ieee

Conference_Titel

Network Protocols, 1993. Proceedings., 1993 International Conference on

Conference_Location

San Francisco, CA

Print_ISBN

0-8186-3670-X

Type

conf

DOI

10.1109/ICNP.1993.340895

Filename

340895