Reducing communication in distributed model checking

Simple item page
dc.contributor.advisorGeldenhuys, Jacoen_ZA
dc.contributor.advisorInggs, Cornelia P.en_ZA
dc.contributor.authorFourie, Jean Francoisen_ZA
dc.contributor.otherUniversity of Stellenbosch. Faculty of Science. Dept. of Mathematical Sciences. Institute for Applied Computer Science.
dc.date.accessioned2009-11-27T11:25:25Zen_ZA
dc.date.accessioned2010-06-01T08:42:11Z
dc.date.available2009-11-27T11:25:25Zen_ZA
dc.date.available2010-06-01T08:42:11Z
dc.date.issued2009-12
dc.descriptionThesis (Msc (Mathematical Sciences. Computer Science))--University of Stellenbosch, 2009.
dc.description.abstractENGLISH 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.en_ZA
dc.description.abstractAFRIKAANSE 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.en_ZA
dc.identifier.urihttp://hdl.handle.net/10019.1/2176
dc.language.isoenen_ZA
dc.publisherStellenbosch : University of Stellenbosch
dc.rights.holderUniversity of Stellenbosch
dc.subjectFormal methodsen_ZA
dc.subjectProgram verificationen_ZA
dc.subjectModel checkingen_ZA
dc.subjectDistributed computingen_ZA
dc.subjectTheses -- Computer scienceen_ZA
dc.subjectDissertations -- Computer scienceen_ZA
dc.subject.lcshComputer systems -- Verificationen_ZA
dc.subject.otherMathematical Sciencesen_ZA
dc.subject.otherComputer Scienceen_ZA
dc.titleReducing communication in distributed model checkingen_ZA
dc.typeThesisen_ZA
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
fourie_reducing_2009.pdf
Size:
733.41 KB
Format:
Adobe Portable Document Format
Description:
Download
Collections
Masters Degrees (Mathematical Sciences)