Reducing communication in distributed model checking

[摘要] ENGLISH ABSTRACT: Model checkers are programs that automatically verify, without human assistance, that certainuser-specified properties hold in concurrent software systems. Since these programs often haveexpensive time and memory requirements, an active area of research is the development of distributedmodel checkers that run on clusters. Of particular interest is how the communicationbetween 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 identifiedand discussed. Furthermore, the implementation of such a program is described. Thecentral idea behind the algorithm is the generation and distribution of data throughout thenodes of the cluster.We introduce several techniques to reduce the communication among the nodes, and studytheir effectiveness by means of a set of models.

[发布机构] Stellenbosch University