A model checker for transition systems

Abstract

A model checker automatically determines whether a model of a reactive system satisfies its specification. Temporal logic is used to specify the intended behaviour of a reactive system which is modelled as a transition system. Fast state space exploration is mandatory, the main problem being to determine the uniqueness of each newly generated state. Traditional model checkers can analyse about 104 states in an acceptable amount of time. A model checker which incorporates three new ideas has been implemented. (1) A bit vector technique used by Holzmann in a fast protocol validation system is combined with model checking to produce a system capable of analysing about 101 reachable states. (2) Since state spaces are sparse and clustered, larger problems are handled by using paging techniques. (3) Traditional model checkers often search subspaces unnecessarily when temporal operators are nested. A top-down technique called subproblem detection is used which avoids this.