An overview and application of model reduction techniques in formal verification

Formal verification methods are becoming increasingly popular in the verification of digital systems and protocol checking of communication systems due to their inherent exhaustive nature. Model checking in particular has become quite extensively used in verifying the performance and functional specification of sequential logic. One characteristic of model checking is the state space explosion problem: as the number of state variables in the model under test increases, state space (and hence CPU/memory consumption of the model checker) increases exponentially. Whereas most previous papers on formal verification dealt largely with theoretical aspects, or were case studies and bug reports, the purpose of this paper is to provide an overview of state space reduction techniques, and then to illustrate several practical manual reduction techniques which have been employed successfully in the model checking of a node controller.