Reducing the state explosion problem during model checking
Date
1991-03
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Stellenbosch : Stellenbosch University
Abstract
ENGLISH ABSTRACT: Our Department is currently engaged in a project to verify concurrent systems. The project is based on the model checking verification technique and a model checker was implemented using transition systems as a modelling language and computation tree logic (CTL) as a specification language. This technique has one serious limitation: the model checker has to generate the reachable state space of a transition system and this state space can be very large. An unmanageable reachable state space is known as a state explosion, and could prohibit the use of model checking for practical concurrent systems.
This thesis investigates the state explosion problem encountered during the model checking of transition systems. A survey of solutions to the state explosion problem is presented from which model reduction is chosen for implementation. Because no reduction methods have been developed for transition systems, a suitable Petri net reduction technique is adapted for the reduction of transition systems. The technique is implemented and proved to correctly reduce a transition system. A summary of performance of the reduction technique is provided.
AFRIKAANSE OPSOMMING: Ons departement is tans betrokke by 'n projek oor die verifikasie van gelyklopende stelsels. Die projek is gebaseer op die modeltoetsing verifikasie-tegniek en 'n modeltoetser is geimplimenteer wat oorgangstelsels as 'n modelleringstaal en temporale logika as 'n spesifikasie-taal gebruik. Hierdie tegniek het 'n ernstige beperking: die modeltoetser moet die bereikbare staatruimte van 'n oorgangstelsel genereer en hierdie staatruimte kan baie groot wees. 'n Onhanteerbare staatruimte staan bekend as 'n staatontploffing, en kan die gebruik van modeltoetsing vir praktiese gelyklopende stelsels keer. Hierdie tesis ondersoek die staatsontploffingsprobleem wat tydens die modeltoetsing van oorgangstelsels ondervind word. 'n Oorsig van oplossings vir die staatsontploffingsprobleem word aangebied waaruit modelreduksie gekies word vir uiteindelike implementasie. Aangesien daar geen reduksie-tegnieke vir oorgangsmodelle bestaan nie, is 'n geskikte Petri net reduksie-tegniek gekies en aangepas vir oorgangstelsels. Die tegniek is geimplementeer en daar word bewys dat 'n oorgangstelsel korrek gereduseer word. 'n Opsomming van reduksie-resultate vir 'n verskeidenheid van voorbeelde word gegee.
AFRIKAANSE OPSOMMING: Ons departement is tans betrokke by 'n projek oor die verifikasie van gelyklopende stelsels. Die projek is gebaseer op die modeltoetsing verifikasie-tegniek en 'n modeltoetser is geimplimenteer wat oorgangstelsels as 'n modelleringstaal en temporale logika as 'n spesifikasie-taal gebruik. Hierdie tegniek het 'n ernstige beperking: die modeltoetser moet die bereikbare staatruimte van 'n oorgangstelsel genereer en hierdie staatruimte kan baie groot wees. 'n Onhanteerbare staatruimte staan bekend as 'n staatontploffing, en kan die gebruik van modeltoetsing vir praktiese gelyklopende stelsels keer. Hierdie tesis ondersoek die staatsontploffingsprobleem wat tydens die modeltoetsing van oorgangstelsels ondervind word. 'n Oorsig van oplossings vir die staatsontploffingsprobleem word aangebied waaruit modelreduksie gekies word vir uiteindelike implementasie. Aangesien daar geen reduksie-tegnieke vir oorgangsmodelle bestaan nie, is 'n geskikte Petri net reduksie-tegniek gekies en aangepas vir oorgangstelsels. Die tegniek is geimplementeer en daar word bewys dat 'n oorgangstelsel korrek gereduseer word. 'n Opsomming van reduksie-resultate vir 'n verskeidenheid van voorbeelde word gegee.
Description
Thesis (M.Sc.)--Stellenbosch University, 1991.
Keywords
Computer programs -- Verification, Programming languages (Electronic computers), Petri nets, Interactive computer systems, Dissertations -- Computer science, UCTD