License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.08332.4
URN: urn:nbn:de:0030-drops-16309
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2008/1630/
Go to the corresponding Portal

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

Efficient Large-Scale Model Checking

pdf-format:
08332.BalHenri.Paper.1630.pdf (0.2 MB)

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:DagSemProc.08332.4,
  author =	{Verstoep, Kees and Bal, Henri E. and Barnat, Jiri and Brim, Lubos},
  title =	{{Efficient Large-Scale Model Checking}},
  booktitle =	{Distributed Verification and Grid Computing},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8332},
  editor =	{Henri E. Bal and Lubos Brim and Martin Leucker},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2008/1630},
  URN =		{urn:nbn:de:0030-drops-16309},
  doi =		{10.4230/DagSemProc.08332.4},
  annote =	{Keywords: Distributed model checking, Grid-based model checking}
}

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

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI