|
Global state reachability analysis is one of the most straight-
forward ways to detect logical errors in communication
protocols specified in the state-transition model. To resolve
the state explosion problem in the global state reachability
analysis, many global state reduction techniques have been
proposed in the past decade. Since context variables are not
considered in most of currently proposed global state reduction
techniques and verification methods, these reduction techniques
and verification methods cannot be directly applied to verify
ECFSM-based protocols. In this thesis, we propose an integrated
ECFSM-based state exploration techniqe which integrates ECFSM-
based fair progress state exploration, ECFSM-based multiple
event one transition state exploration, an ECFSM-based
incremental verification technique, and the concept of dead and
live variables introduced by Chu and Liu, to have a new
verification technique for ECFSM-based protocols. Using the
integrated ECFSM-based state exploration technique, we have
developed an Integrated Estelle-based Incremental Protocol
Verification System (IEIPVS) in a SUN SPARC 10 workstation.
IEIPVS consists of three main components, i.e., the Estelle
interpreter, global state analyzer based on the integrated
ECFSM-based state exploration for exploring stable/unstable
global states, and the incremental verification processor. With
a friendly graphical user interface provided in IEIPVS,
prototol designers can interactively specify and incrementally
verify protocols with our proposed global state reduction
technique.
|