Full Text Available
Note: Clicking the button above will open the full text document at the original institutional repository in a new window.
A model checker for the LF system
Thesis (MSc)--University of Stellenbosch, 2007.
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_ | 1867613902439710720 |
|---|---|
| access_status_str | Open Access |
| author | Gerber, Erick D. B. |
| author2 | Geldenhuys, J. |
| author_browse | Geldenhuys, J. Gerber, Erick D. B. |
| author_facet | Geldenhuys, J. Gerber, Erick D. B. |
| author_sort | Gerber, Erick D. B. |
| collection | Thesis |
| dc_rights_str_mv | Stellenbosch University |
| description | Thesis (MSc)--University of Stellenbosch, 2007. |
| format | Thesis |
| id | oai:scholar.sun.ac.za:10019.1/19597 |
| institution | Stellenbosch University (South Africa) |
| language | en_ZA |
| last_indexed | 2026-06-10T12:43:31.605Z |
| 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/19597 A model checker for the LF system Gerber, Erick D. B. Geldenhuys, J. Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences. Institute for Applied Computer Science. Computer programs -- Verification Computer software -- Verification Computer software -- Reliability Computer simulation Programming languages (Electronic computers) Theses -- Computer science Dissertations -- Computer science Thesis (MSc)--University of Stellenbosch, 2007. ENGLISH ABSTRACT: Computer aided veri cation techniques, such as model checking, can be used to improve the reliability of software. Model checking is an algorithmic approach to illustrate the correctness of temporal logic speci cations in the formal description of hardware and software systems. In contrast to traditional testing tools, model checking relies on an exhaustive search of all the possible con gurations that these systems may exhibit. Traditionally model checking is applied to abstract or high level designs of software. However, often interpreting or translating these abstract designs to implementations introduce subtle errors. In recent years one trend in model checking has been to apply the model checking algorithm directly to the implementations instead. This thesis is concerned with building an e cient model checker for a small concurrent langauge developed at the University of Stellenbosch. This special purpose langauge, LF, is aimed at developement of small embedded systems. The design of the language was carefully considered to promote safe programming practices. Furthermore, the language and its runtime support system was designed to allow directly model checking LF programs. To achieve this, the model checker extends the existing runtime support infrastructure to generate the state space of an executing LF program. AFRIKAANSE OPSOMMING: Rekenaar gebaseerde program toetsing, soos modeltoetsing, kan gebruik word om die betroubaarheid van sagteware te verbeter. Model toetsing is 'n algoritmiese benadering om die korrektheid van temporale logika spesi kasies in die beskrywing van harde- of sagteware te bewys. Anders as met tradisionlee program toetsing, benodig modeltoetsing 'n volledige ondersoek van al die moontlike toestande waarin so 'n beskrywing homself kan bevind. Model toetsing word meestal op abstrakte modelle van sagteware of die ontwerp toegepas. Indien die ontwerp of model aan al die spesi kasies voldoen word die abstrakte model gewoontlik vertaal na 'n implementasie. Die vertalings proses word gewoontlik met die hand gedoen en laat ruimte om nuwe foute, en selfs foute wat uitgeskakel in die model of ontwerp is te veroorsaak. Deesdae, is 'n gewilde benadering tot modeltoetsing om di e tegnieke direk op die implementasie toe te pas, en sodoende die ekstra moeite van model konstruksie en vertaling uit te skakel. Hierdie tesis handel oor die ontwerp, implementasie en toetsing van 'n e ektiewe modeltoetser vir 'n klein gelyklopende taal, LF, wat by die Universiteit van Stellenbosch ontwikkel is. Die enkeldoelige taal, LF, is gemik op die veilige ontwikkeling van ingebedde sagteware. Die taal is ontwerp om veilige programmerings praktyke aan te moedig. Verder is die taal en die onderliggende bedryfstelsel so ontwerp om 'n model toetser te akkomodeer. Om die LF programme direk te kan toets, is die model toetser 'n integrale deel van die bedryfstelsel sodat dit die program kan aandryf om alle moontlike toestande te besoek. 2012-02-07T10:09:41Z 2012-02-07T10:09:41Z 2007-03 Thesis http://hdl.handle.net/10019.1/19597 en_ZA Stellenbosch University xi, 92 leaves : ill. application/pdf Stellenbosch : Stellenbosch University |
| spellingShingle | Computer programs -- Verification Computer software -- Verification Computer software -- Reliability Computer simulation Programming languages (Electronic computers) Theses -- Computer science Dissertations -- Computer science Gerber, Erick D. B. A model checker for the LF system |
| title | A model checker for the LF system |
| title_full | A model checker for the LF system |
| title_fullStr | A model checker for the LF system |
| title_full_unstemmed | A model checker for the LF system |
| title_short | A model checker for the LF system |
| title_sort | model checker for the lf system |
| topic | Computer programs -- Verification Computer software -- Verification Computer software -- Reliability Computer simulation Programming languages (Electronic computers) Theses -- Computer science Dissertations -- Computer science |
| url | http://hdl.handle.net/10019.1/19597 |
| work_keys_str_mv | AT gerbererickdb amodelcheckerforthelfsystem AT gerbererickdb modelcheckerforthelfsystem |