Reducing the state explosion problem during model checking

Simple item page
dc.contributor.advisorDe Villiers, P. J. A.en_ZA
dc.contributor.advisorKrzesinkski, A. E.en_ZA
dc.contributor.authorBarnard, Dieter Corneliusen_ZA
dc.contributor.otherStellenbosch University. Faculty of Science. Dept. of Mathematical Sciences. Division Computer Science.en_ZA
dc.date.accessioned2012-08-27T12:27:03Z
dc.date.available2012-08-27T12:27:03Z
dc.date.issued1991-03
dc.descriptionThesis (M.Sc.)--Stellenbosch University, 1991.
dc.description.abstractENGLISH 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.en_ZA
dc.description.abstractAFRIKAANSE 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.af_ZA
dc.format.extent139 pages : illustrations.
dc.identifier.urihttp://hdl.handle.net/10019.1/69386
dc.language.isoen_ZA
dc.publisherStellenbosch : Stellenbosch University
dc.rights.holderStellenbosch University
dc.subjectComputer programs -- Verificationen_ZA
dc.subjectProgramming languages (Electronic computers)en_ZA
dc.subjectPetri netsen_ZA
dc.subjectInteractive computer systemsen_ZA
dc.subjectDissertations -- Computer scienceen_ZA
dc.subjectUCTDen_ZA
dc.titleReducing the state explosion problem during model checkingen_ZA
dc.typeThesis
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
barnard_reducing_1991.pdf
Size:
25.68 MB
Format:
Adobe Portable Document Format
Description:
Download thesis
Download
Collections
Masters Degrees (Computer Science)