Full Text Available
Note: Clicking the button above will open the full text document at the original institutional repository in a new window.
Reducing the state explosion problem during model checking
Thesis (M.Sc.)--Stellenbosch University, 1991.
Saved in:
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | en_ZA |
| Published: |
Stellenbosch : Stellenbosch University
2012
|
| Subjects: | |
| Tags: |
No Tags, Be the first to tag this record!
|
| _version_ | 1867613952556400641 |
|---|---|
| access_status_str | Open Access |
| author | Barnard, Dieter Cornelius |
| author2 | De Villiers, P. J. A. |
| author_browse | Barnard, Dieter Cornelius De Villiers, P. J. A. |
| author_facet | De Villiers, P. J. A. Barnard, Dieter Cornelius |
| author_sort | Barnard, Dieter Cornelius |
| collection | Thesis |
| dc_rights_str_mv | Stellenbosch University |
| description | Thesis (M.Sc.)--Stellenbosch University, 1991. |
| format | Thesis |
| id | oai:scholar.sun.ac.za:10019.1/69386 |
| institution | Stellenbosch University (South Africa) |
| language | en_ZA |
| last_indexed | 2026-06-10T12:44:19.493Z |
| license_str | Other — see source repository |
| provenance_str_mv | Harvested via OAI-PMH from SUNScholar — Stellenbosch University Repository |
| publishDate | 2012 |
| publishDateRange | 2012 |
| publishDateSort | 2012 |
| publisher | Stellenbosch : Stellenbosch University |
| publisherStr | Stellenbosch : Stellenbosch University |
| record_format | dspace |
| source_str | SUNScholar — Stellenbosch University Repository |
| spelling | oai:scholar.sun.ac.za:10019.1/69386 Reducing the state explosion problem during model checking Barnard, Dieter Cornelius De Villiers, P. J. A. Krzesinkski, A. E. Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences. Division Computer Science. Computer programs -- Verification Programming languages (Electronic computers) Petri nets Interactive computer systems Dissertations -- Computer science UCTD Thesis (M.Sc.)--Stellenbosch University, 1991. 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. 2012-08-27T12:27:03Z 2012-08-27T12:27:03Z 1991-03 Thesis http://hdl.handle.net/10019.1/69386 en_ZA Stellenbosch University 139 pages : illustrations. application/pdf Stellenbosch : Stellenbosch University |
| spellingShingle | Computer programs -- Verification Programming languages (Electronic computers) Petri nets Interactive computer systems Dissertations -- Computer science UCTD Barnard, Dieter Cornelius Reducing the state explosion problem during model checking |
| title | Reducing the state explosion problem during model checking |
| title_full | Reducing the state explosion problem during model checking |
| title_fullStr | Reducing the state explosion problem during model checking |
| title_full_unstemmed | Reducing the state explosion problem during model checking |
| title_short | Reducing the state explosion problem during model checking |
| title_sort | reducing the state explosion problem during model checking |
| topic | Computer programs -- Verification Programming languages (Electronic computers) Petri nets Interactive computer systems Dissertations -- Computer science UCTD |
| url | http://hdl.handle.net/10019.1/69386 |
| work_keys_str_mv | AT barnarddietercornelius reducingthestateexplosionproblemduringmodelchecking |