Protocol verification using symbolic model checking

• Main Author: Mathieson, Charles G.
• Format: Others
• Language: English
• Published: 2009
• Online Access: http://hdl.handle.net/2429/4956

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