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 Stand
ardization for protocol specifications. We present an incremental prot
ocol design system that contains an incremental protocol verification
technique and an Estelle translator. Our incremental protocol design s
ystem allows on-line reverification after respecification. That is, in
stead of verifying respecified (modified) protocols from scratch, the
reverification procedure is executed continuously and incrementally at
the modification point. Using the translator, Estelle protocol specif
ications can be translated and interpreted for protocol verification.
To meet the requirement of modifying protocol specifications written i
n Estelle at run time, the Estelle translator allows incremental trans
lation and interpretation of the modified Estelle specification part f
or incremental verification. To further reduce the number of global st
ates to be explored, the concept of dead and live variables is incorpo
rated into our incremental verification technique. Based on the increm
ental verification technique and the Estelle translator, an incrementa
l protocol design system (IPDS) is developed on SUN SPARC OPENLOOK wor
kstations. Using IPDS, protocol designers can analyze the verification
results, interactively modify the protocols, and then continue the ve
rification incrementally. (C) 1997 by Elsevier Science Inc.