Full Text Available
Note: Clicking the button above will open the full text document at the original institutional repository in a new window.
Reducing communication in distributed model checking
Thesis (Msc (Mathematical Sciences. Computer Science))--University of Stellenbosch, 2009.
Saved in:
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | English |
| Published: |
Stellenbosch : University of Stellenbosch
2009
|
| Subjects: | |
| Tags: |
No Tags, Be the first to tag this record!
|
| _version_ | 1867613801092743168 |
|---|---|
| access_status_str | Open Access |
| author | Fourie, Jean Francois |
| author2 | Geldenhuys, Jaco |
| author_browse | Fourie, Jean Francois Geldenhuys, Jaco |
| author_facet | Geldenhuys, Jaco Fourie, Jean Francois |
| author_sort | Fourie, Jean Francois |
| collection | Thesis |
| dc_rights_str_mv | University of Stellenbosch |
| description | Thesis (Msc (Mathematical Sciences. Computer Science))--University of Stellenbosch, 2009. |
| format | Thesis |
| id | oai:scholar.sun.ac.za:10019.1/2176 |
| institution | Stellenbosch University (South Africa) |
| language | English |
| last_indexed | 2026-06-10T12:41:54.752Z |
| license_str | Other — see source repository |
| provenance_str_mv | Harvested via OAI-PMH from SUNScholar — Stellenbosch University Repository |
| publishDate | 2009 |
| publishDateRange | 2009 |
| publishDateSort | 2009 |
| publisher | Stellenbosch : University of Stellenbosch |
| publisherStr | Stellenbosch : University of Stellenbosch |
| record_format | dspace |
| source_str | SUNScholar — Stellenbosch University Repository |
| spelling | oai:scholar.sun.ac.za:10019.1/2176 Reducing communication in distributed model checking Fourie, Jean Francois Geldenhuys, Jaco Inggs, Cornelia P. University of Stellenbosch. Faculty of Science. Dept. of Mathematical Sciences. Institute for Applied Computer Science. Formal methods Program verification Model checking Distributed computing Theses -- Computer science Dissertations -- Computer science Computer systems -- Verification Mathematical Sciences Computer Science Thesis (Msc (Mathematical Sciences. Computer Science))--University of Stellenbosch, 2009. ENGLISH ABSTRACT: Model checkers are programs that automatically verify, without human assistance, that certain user-specified properties hold in concurrent software systems. Since these programs often have expensive time and memory requirements, an active area of research is the development of distributed model checkers that run on clusters. Of particular interest is how the communication between the machines can be reduced to speed up their running time. In this thesis the design decisions involved in an on-the-fly distributed model checker are identified and discussed. Furthermore, the implementation of such a program is described. The central idea behind the algorithm is the generation and distribution of data throughout the nodes of the cluster. We introduce several techniques to reduce the communication among the nodes, and study their effectiveness by means of a set of models. AFRIKAANSE OPSOMMING: Modeltoetsers is programme wat outomaties bevestig, sonder enige hulp van die gebruiker, dat gelopende sagteware aan sekere gespesifiseerde eienskappe voldoen. Die feit dat hierdie programme dikwels lang looptye en groot geheues benodig, het daartoe aanleiding gegee dat modeltoetsers wat verspreid oor ’n groep rekenaars hardloop, aktief nagevors word. Dit is veral belangrik om vas te stel hoe die kommunikasie tussen rekenaars verminder kan word om sodoende die looptyd te verkort. Hierdie tesis identifiseer en bespreek die ontwerpsbesluite betrokke in die ontwikkeling van ’n verspreide modeltoetser. Verder word die implementasie van so ’n program beskryf. Die kernidee is die generasie en verspreiding van data na al die rekenaars in die groep wat aan die probleem werk. Ons stel verskeie tegnieke voor om die kommunikasie tussen die rekenaar te verminder en bestudeer die effektiwiteit van hierdie tegnieke aan die hand van ’n lys modelle. 2009-11-27T11:25:25Z 2010-06-01T08:42:11Z 2009-11-27T11:25:25Z 2010-06-01T08:42:11Z 2009-12 Thesis http://hdl.handle.net/10019.1/2176 en University of Stellenbosch application/pdf Stellenbosch : University of Stellenbosch |
| spellingShingle | Formal methods Program verification Model checking Distributed computing Theses -- Computer science Dissertations -- Computer science Computer systems -- Verification Mathematical Sciences Computer Science Fourie, Jean Francois Reducing communication in distributed model checking |
| title | Reducing communication in distributed model checking |
| title_full | Reducing communication in distributed model checking |
| title_fullStr | Reducing communication in distributed model checking |
| title_full_unstemmed | Reducing communication in distributed model checking |
| title_short | Reducing communication in distributed model checking |
| title_sort | reducing communication in distributed model checking |
| topic | Formal methods Program verification Model checking Distributed computing Theses -- Computer science Dissertations -- Computer science Computer systems -- Verification Mathematical Sciences Computer Science |
| url | http://hdl.handle.net/10019.1/2176 |
| work_keys_str_mv | AT fouriejeanfrancois reducingcommunicationindistributedmodelchecking |