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.
| Identifer | oai:union.ndltd.org:netd.ac.za/oai:union.ndltd.org:sun/oai:scholar.sun.ac.za:10019.1/2176 |
| Date | 12 1900 |
| Creators | Fourie, Jean Francois |
| Contributors | Geldenhuys, Jaco, Ingg, Cornelia, University of Stellenbosch. Faculty of Science. Dept. of Mathematical Sciences. Institute for Applied Computer Science. |
| Publisher | Stellenbosch : University of Stellenbosch |
| Source Sets | South African National ETD Portal |
| Language | English |
| Detected Language | Unknown |
| Type | Thesis |
| Rights | University of Stellenbosch |
Page generated in 0.002 seconds