A model checker for transition systems
Loading...
Authors
De Villiers, PJA
Issue Date
1991
Type
Language
en
Keywords
Alternative Title
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 107 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.
Description
Citation
De Villiers, P.J.A. (1991) A model checker for transition systems. Proceedings of the 6th Southern African Computer Symposium, De Overberger Hotel, Caledon, 2-3 July 1991