Institutional Repository

A model checker for transition systems

Show simple item record

dc.contributor.author De Villiers, PJA
dc.contributor.editor Linck, M.H.
dc.date.accessioned 2018-08-13T11:59:42Z
dc.date.available 2018-08-13T11:59:42Z
dc.date.issued 1991
dc.identifier.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 en
dc.identifier.uri http://hdl.handle.net/10500/24581
dc.description.abstract A model checker automatically determines whether a model of a re­active system satisfies its specification.Temporal logic is used to spec­ify 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 check­ers often search subspaces unnecessarily when temporal operators are nested. A top-down technique called subproblem detection is used which avoids this. en
dc.language.iso en en
dc.title A model checker for transition systems en


Files in this item

This item appears in the following Collection(s)

Show simple item record

Search UnisaIR


Browse

My Account

Statistics