Reducing communication in distributed model checking
Date
2009-12
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Stellenbosch : University of Stellenbosch
Abstract
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.
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.
Description
Thesis (Msc (Mathematical Sciences. Computer Science))--University of Stellenbosch, 2009.
Keywords
Formal methods, Program verification, Model checking, Distributed computing, Theses -- Computer science, Dissertations -- Computer science