VERSTOEP, Kees, Henri E. BAL, Jiří BARNAT a Luboš BRIM. Efficient Large-Scale Model Checking. In 23rd IEEE International Parallel & Distributed Processing Symposium. IEEE: IEEE, 2009. s. 201-212, 12 s. ISBN 978-1-4244-3751-1.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Efficient Large-Scale Model Checking
Název česky Efektivní verifikace rosáhlých modelů
Autoři VERSTOEP, Kees (528 Nizozemsko), Henri E. BAL (528 Nizozemsko), Jiří BARNAT (203 Česká republika, garant, domácí) a Luboš BRIM (203 Česká republika, domácí).
Vydání IEEE, 23rd IEEE International Parallel & Distributed Processing Symposium, od s. 201-212, 12 s. 2009.
Nakladatel IEEE
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Itálie
Utajení není předmětem státního či obchodního tajemství
Kód RIV RIV/00216224:14330/09:00029324
Organizační jednotka Fakulta informatiky
ISBN 978-1-4244-3751-1
ISSN 1530-2075
UT WoS 000272993600019
Klíčová slova anglicky model checking; distributed; parallel; large-scale
Štítky distributed, large-scale, Model checking, parallel
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: prof. RNDr. Luboš Brim, CSc., učo 197. Změněno: 2. 2. 2011 09:34.
Anotace
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.
Anotace česky
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í.
Návaznosti
GA201/09/1389, projekt VaVNázev: Verifikace a analýza velmi velkých počítačových systémů
Investor: Grantová agentura ČR, Standardní projekty
GP201/09/P497, projekt VaVNázev: Automatizovaná formální verifikace s využitím soudobého hardware
Investor: Grantová agentura ČR, Postdoktorské projekty
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumné záměry
VytisknoutZobrazeno: 25. 9. 2020 02:06