VERSTOEP, Kees, Henri E. BAL, Jiří BARNAT and Luboš BRIM. Efficient Large-Scale Model Checking. In 23rd IEEE International Parallel & Distributed Processing Symposium. IEEE: IEEE. p. 201-212. ISBN 978-1-4244-3751-1. 2009.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Efficient Large-Scale Model Checking
Name in Czech Efektivní verifikace rosáhlých modelů
Authors VERSTOEP, Kees (528 Netherlands), Henri E. BAL (528 Netherlands), Jiří BARNAT (203 Czech Republic, guarantor, belonging to the institution) and Luboš BRIM (203 Czech Republic, belonging to the institution).
Edition IEEE, 23rd IEEE International Parallel & Distributed Processing Symposium, p. 201-212, 12 pp. 2009.
Publisher IEEE
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Italy
Confidentiality degree is not subject to a state or trade secret
RIV identification code RIV/00216224:14330/09:00029324
Organization unit Faculty of Informatics
ISBN 978-1-4244-3751-1
ISSN 1530-2075
UT WoS 000272993600019
Keywords in English model checking; distributed; parallel; large-scale
Tags distributed, large-scale, Model checking, parallel
Tags International impact, Reviewed
Changed by Changed by: prof. RNDr. Luboš Brim, CSc., učo 197. Changed: 2/2/2011 09:34.
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, 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.
Abstract (in Czech)
Model checking je populární technika používaná pro analýzu a verifikaci systémů. Boužel její použití je limitováno problémem stavové exploze. Nástroje, které překonávají tento problém s použitím prostředí distribuovanou pamětí existují, byly ale testovány pouze na malých klastrech. V tomto článku je navrženo několik obecných technik, které umožňují efektivní využití výpočetních zdrojů i v případě použití rozsáhlých systémů s distribuovanou pamětí.
Links
GA201/09/1389, research and development projectName: Verifikace a analýza velmi velkých počítačových systémů
Investor: Czech Science Foundation, Verification and Analysis of Large-Scale Computer Systems
GP201/09/P497, research and development projectName: Automatizovaná formální verifikace s využitím soudobého hardware
Investor: Czech Science Foundation, Automated formal verification using modern hardware
MSM0021622419, plan (intention)Name: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems
PrintDisplayed: 29/3/2024 09:13