Other formats:
BibTeX
LaTeX
RIS
@inproceedings{834666, author = {Verstoep, Kees and Bal, Henri E. and Barnat, Jiří and Brim, Luboš}, address = {IEEE}, booktitle = {23rd IEEE International Parallel & Distributed Processing Symposium}, keywords = {model checking; distributed; parallel; large-scale}, language = {eng}, location = {IEEE}, isbn = {978-1-4244-3751-1}, pages = {201-212}, publisher = {IEEE}, title = {Efficient Large-Scale Model Checking}, year = {2009} }
TY - JOUR ID - 834666 AU - Verstoep, Kees - Bal, Henri E. - Barnat, Jiří - Brim, Luboš PY - 2009 TI - Efficient Large-Scale Model Checking PB - IEEE CY - IEEE SN - 9781424437511 KW - model checking KW - distributed KW - parallel KW - large-scale N2 - 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, DiVinE, 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. ER -
VERSTOEP, Kees, Henri E. BAL, Jiří BARNAT and Luboš BRIM. Efficient Large-Scale Model Checking. In \textit{23rd IEEE International Parallel \&{} Distributed Processing Symposium}. IEEE: IEEE, 2009, p.~201-212. ISBN~978-1-4244-3751-1.
|