Scalable shared memory LTL model checking

BARNAT, Jiří; Luboš BRIM a Petr ROČKAI. Scalable shared memory LTL model checking. International Journal on Software Tools for Technology Transfer (STTT). Springer-Verlag GmbH, 2010, roč. 12, č. 2, s. 139-153. ISSN 1433-2779. Dostupné z: https://doi.org/10.1007/s10009-010-0136-z.

Základní údaje

Originální název

Scalable shared memory LTL model checking

Autoři

BARNAT, Jiří; Luboš BRIM a Petr ROČKAI

Vydání

International Journal on Software Tools for Technology Transfer (STTT), Springer-Verlag GmbH, 2010, 1433-2779

---

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Odkazy

URL

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/10:00065778

Organizační jednotka

Fakulta informatiky

DOI

https://doi.org/10.1007/s10009-010-0136-z

Klíčová slova anglicky

LTL Model Cecking; Parallel; Shared-Memory

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

Recent development in computer hardware has brought more wide-spread emergence of shared memory, multi-core systems. These architectures offer opportunities to speed up various tasks - model checking and reachability analysis among others. In this paper, we present a design for a parallel shared memory LTL model checker that is based on a distributed memory algorithm. To improve the scalability of our tool, we have devised a number of implementation techniques which we present in this paper. We also report on a number of experi- ments we conoducted to analyze the behaviour of our tool under different conditions using various models. We demonstrate that our tool exhibits significant speedup in comparison to sequential tools, which improves the workflow of verification in general.

Česky

Nedávný vývoj v oblasti počítačového HW vedl k masovému rozšíření vícekórových výpočetních systémů. Tyto systémy umožňují akceleraci různých úloh paralelizací. V článku je popsán návrh paralelního nástroje pro LTL ověřování modelu. Paralelní škálovatelnost nástroje je umocněna nově navrhnutými implementačními technikami. Nástroj byl pro účely článku experimentálně evaluován na několika modelech, zpráva o této evaluaci je součástí článku. Nástroj vykazuje vzhledem k své sekvenční verzi významné zrychlení procesu verifikace.

---

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
MUNI/A/0914/2009, interní kód MU	Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV) Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
1ET408050503, projekt VaV	Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů
1M0545, projekt VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky