Verstoep, Kees ;
Bal, Henri E. ;
Barnat, Jiri ;
Brim, Lubos
Efficient Large-Scale Model Checking
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 |
30.10.2008
