Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH scholarly article en Verstoep, Kees; Bal, Henri E.; Barnat, Jiri; Brim, Lubos License
when quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-16309

; ; ;

Efficient Large-Scale Model Checking



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

  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 =		{},
  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 | Privacy Published by LZI