A model checker for transition systems
Authors
De Villiers, PJA
Issue Date
1992
Type
Article
Language
en
Keywords
Verification , Transition systems , Branching time temporal logic , Model checking
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 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.
Description
Citation
De Villiers PJA (1992) A model checker for transition systems. South African Computer Journal, Number 8, 1992
Publisher
South African Computer Society (SAICSIT)
License
Journal
Volume
Issue
PubMed ID
DOI
ISSN
2313-7835