Full Text Available
Note: Clicking the button above will open the full text document at the original institutional repository in a new window.
Efficiency issues in the design of a model checker
Thesis (M.Sc.) -- University of Stellenbosch, 1999.
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_ | 1867613803404853248 |
|---|---|
| access_status_str | Open Access |
| author | Geldenhuys, Jacobus |
| author2 | De Villiers, P. J. A. |
| author_browse | De Villiers, P. J. A. Geldenhuys, Jacobus |
| author_facet | De Villiers, P. J. A. Geldenhuys, Jacobus |
| author_sort | Geldenhuys, Jacobus |
| collection | Thesis |
| dc_rights_str_mv | Stellenbosch University |
| description | Thesis (M.Sc.) -- University of Stellenbosch, 1999. |
| format | Thesis |
| id | oai:scholar.sun.ac.za:10019.1/51253 |
| institution | Stellenbosch University (South Africa) |
| language | en_ZA |
| last_indexed | 2026-06-10T12:41:57.021Z |
| 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/51253 Efficiency issues in the design of a model checker Geldenhuys, Jacobus De Villiers, P. J. A. Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences. Computer algorithms Programming languages (Electronic computers) ESML modelling language Dissertations -- Computer science Thesis (M.Sc.) -- University of Stellenbosch, 1999. ENGLISH SUMMARY: A model checker is a program that verifies, without human assistance, that the formal description of a system has specified, desirable properties. The development of model checking algorithms is an active area of research, but most implementations are still prototypical in nature. In consequence, knowledge about the design and implementation of a practical, efficient model checker is limited. In this thesis the most important design decisions involved in creating an efficient on-the-fly model checker are identified and discussed. In short, there are three major tasks: 1. the generation of program states, 2. the detection of revisited states, and 3. the representation of states. In all three cases the central goal is to generate as many states as possible and to generate states as fast as possible. For each task, alternatives are described and compared. The discussion of design issues is further supported in two ways. First, a detailed design and implementation for a model checker is described to illustrate how design decisions affect each other and ultimately the implementation. Second, the design arguments, based on more or less realistic models, are validated through a thorough study of the performance of the various components of the model checker. AFRIKAANSE OPSOMMING: 'n Modeltoetser is 'n program wat vasstel of die formele beskrywing van 'n stelsel oor wenslike, vooraf-gespesifiseerde eienskappe beskik. Die ontwikkeling van algoritmes vir hierdie doel word aktief nagevors, maar in die meeste gevalle is implementasies van modeltoetsers van 'n bloot prototipiese aard. Gevolglik is kennis oor die ontwerp en implementering van 'n praktiese, effektiewe modeltoetser so skaars soos hoendertande. Hierdie tesis bespreek die belangrikste ontwerpsbesluite in die ontwikkeling van 'n effektiewe modeltoetser. Drie hooftake word geldentifiseer: 1. die voortbrengs van state (programtoestande), 2. die herkenning van reeds bekende state, en 3. die interne voorstelling van state. In al drie gevalle is die belangrikste doelwit om so veel as moontlik state voort te bring, en om state so vinnig as moontlik voort te bring. Vir elke taak word alternatiewe bespreek en vergelyk. Die bespreking word verder op twee maniere ondersteun. Eerstens word 'n modeltoetser se ontwerp en implementasie in detail beskryf om die invloed van ontwerpsbesluite op mekaar en op die uiteindelike implementasie te illustreer. Tweedens word die argumente, tot dusver gebaseer op redelike aannames, gevalideer deur 'n deeglike studie van die werkverrigting van die modeltoetser se onderskeie onderdele. Master 2012-08-27T11:34:24Z 2012-08-27T11:34:24Z 1999-11 Thesis http://hdl.handle.net/10019.1/51253 en_ZA Stellenbosch University 139 pages : ill. application/pdf Stellenbosch : Stellenbosch University |
| spellingShingle | Computer algorithms Programming languages (Electronic computers) ESML modelling language Dissertations -- Computer science Geldenhuys, Jacobus Efficiency issues in the design of a model checker |
| title | Efficiency issues in the design of a model checker |
| title_full | Efficiency issues in the design of a model checker |
| title_fullStr | Efficiency issues in the design of a model checker |
| title_full_unstemmed | Efficiency issues in the design of a model checker |
| title_short | Efficiency issues in the design of a model checker |
| title_sort | efficiency issues in the design of a model checker |
| topic | Computer algorithms Programming languages (Electronic computers) ESML modelling language Dissertations -- Computer science |
| url | http://hdl.handle.net/10019.1/51253 |
| work_keys_str_mv | AT geldenhuysjacobus efficiencyissuesinthedesignofamodelchecker |