License
When quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-16309
URL: http://drops.dagstuhl.de/opus/volltexte/2008/1630/
Go to the corresponding Portal


Verstoep, Kees ; Bal, Henri E. ; Barnat, Jiri ; Brim, Lubos

Efficient Large-Scale Model Checking

pdf-format:
Document 1.pdf (156 KB)


Abstract

Model checking is a popular technique to systematically and automatically verify system properties. Unfortunately, the well-known state explosion problem often limits the extent to which it can be applied to realistic specifications, due to the huge resulting memory requirements. Distributed memory model checkers exist, but have thus far only been evaluated on small-scale clusters, with mixed results. We examine one well-known distributed model checker in detail, and show how a number of additional optimizations in its runtime system enable it to efficiently check very demanding problem instances on a large-scale, multi-core compute cluster. We analyze the impact of the distributed algorithms employed, the problem instance characteristics and network overhead. Finally, we show that the model checker can even obtain good performance in a high-bandwidth computational grid environment.

BibTeX - Entry

@InProceedings{verstoep_et_al:DSP:2008:1630,
  author =	{Kees Verstoep and Henri E. Bal and Jiri Barnat and Lubos Brim},
  title =	{Efficient Large-Scale Model Checking},
  booktitle =	{Distributed Verification and Grid Computing },
  year =	{2008},
  editor =	{Henri E. Bal and Lubos Brim and Martin Leucker},
  number =	{08332},
  series =	{Dagstuhl Seminar Proceedings},
  ISSN =	{1862-4405},
  publisher =	{Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2008/1630},
  annote =	{Keywords: Distributed model checking, Grid-based model checking}
}

Keywords: Distributed model checking, Grid-based model checking
Seminar: 08332 - Distributed Verification and Grid Computing
Issue Date: 2008
Date of publication: 30.10.2008


DROPS-Home | Fulltext Search | Imprint Published by LZI