| Summary: | To reduce problems encountered in the later phases of the
software life cycle, verification techniques can be used in the
design phase to ensure that a design has the intended
properties. The main advantage of using formal verification
over other validation methods, such as simulation and testing,
is that it reasons about all possible behaviours of a system.
However, formal verification techniques have not yet been widely
accepted in industry because most of them suffer from the state
explosion problem or are too difficult to use.
In this thesis, an automatic model checking verification
system for communication protocols is developed that tackles the
state explosion problem. The Ever symbolic verifier [HDDY92],
which is a high-level specification language and symbolic
reachability analysis tool for extended finite state machines,
is used as a basis for this system. The system accepts a
protocol specification written in Estelle.Y [Lu91], a variant of
the Estelle formal protocol description language [IS089]. Each
Estelle.Y module of the specification is translated into the
Ever language and fed into the Ever symbolic verifier. The
intended properties are written as CTL temporal logic formulae
[CG87] expressed in terms of variables in the Estelle.Y
specifications. These formulae are given to the verifier to check that they are true in the model produced from the protocol
specification. With this system one can assert that given
safety and liveness properties are true in all possible
behaviours of a protocol. When the system finds a given formula
to be false, it is capable of producing a counterexample trace.
This trace greatly assists the designer to correct the protocol
specification and the temporal formulae of the intended
properties.
After the Estelle.Y to Ever translator was implemented, the
original Ever verifier was extended to support model checking of
CTL temporal formulae [CG87]. The extended verifier can check
not only eventuality properties but also more general temporal
properties such as precedences and invariances. The Ever
verifier was also extended with the notion of fairness
constraints [BCMD90] to allow the model to check only fair
behaviours. These extensions enable incremental verification to
be performed to reduce the overall checking time dramatically.
This system was successfully applied to the specification of
the alternating bit protocol [IS089] to demonstrate this new
tool. Various safety and liveness properties expressed as CTL
temporal formulae are described and explained in detail in this
thesis. The CPU time and memory requirements for this
verification are discussed. === Science, Faculty of === Computer Science, Department of === Graduate
|
|---|
