Efficient Large-Scale Model Checking

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. ISBN 978-1-4244-3751-1.

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 Nizozemské království), Henri E. BAL (528 Nizozemské království), 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

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

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

---

Anotace

V originále

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.

Č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 VaV	Název: Verifikace a analýza velmi velkých počítačových systémů Investor: Grantová agentura ČR, Verifikace a analýza velmi velkých počítačových systémů
GP201/09/P497, projekt VaV	Název: Automatizovaná formální verifikace s využitím soudobého hardware Investor: Grantová agentura ČR, Automatizovaná formální verifikace s využitím soudobého hardware
MSM0021622419, záměr	Název: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy