An Estelle translator for incremental protocol verification

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.