DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking

BARNAT, Jiří, Luboš BRIM a Milan ČEŠKA. DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking. Electronic Proceedings in Theoretical Computer Science. 2009, roč. 14, Prosinec, s. 107--111. ISSN 2075-2180.

Základní údaje

• Originální název: DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking
• Název česky: DiVinE-CUDA - Nástroj pro GPU akcelerované ověřování modelu LTL
• Autoři: BARNAT, Jiří (203 Česká republika, garant, domácí), Luboš BRIM (203 Česká republika, domácí) a Milan ČEŠKA (203 Česká republika, domácí).
• Vydání: Electronic Proceedings in Theoretical Computer Science, 2009, 2075-2180.

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Článek v odborném periodiku
• Obor: 10201 Computer sciences, information science, bioinformatics
• Stát vydavatele: Nizozemské království
• Utajení: není předmětem státního či obchodního tajemství
• WWW: URL
• Kód RIV: RIV/00216224:14330/09:00028691
• Organizační jednotka: Fakulta informatiky
• Klíčová slova česky: LTL; Ověřování modelu; CUDA
• Klíčová slova anglicky: LTL; Model Checking; CUDA
• Příznaky: Mezinárodní význam, Recenzováno

Anotace

In this paper we present a tool that performs CUDA accelerated LTL Model Checking. The tool exploits parallel algorithm MAP adjusted to the NVIDIA CUDA architecture in order to efficiently detect the presence of accepting cycles in a directed graph. Accepting cycle detection is the core algorithmic procedure in automata-based LTL Model Checking. We demonstrate that the tool outperforms non-accelerated version of the algorithm and we discuss where the limits of the tool are and what we intend to do in the future to avoid them.

Anotace česky

V tomto čláku prezentujeme nástroj, který provádí CUDA akcelerované ověřování modelu logiky LTL. Nástroj staví na paralelním algoritmu MAP upraveném pro platformu NVIDIA CUDA. Demonstrujeme, že verifikace je s použitím nástroje výrazně rychlejší než bez použití dané architektury. V článku identifikujeme některé problémy, které s realizací nástroje souvisí a diskutujeme, jak je možné tyto problémy řešit v budoucnosti.

Návaznosti

• GD102/09/H042, projekt VaV: Název: Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů

Investor: Grantová agentura ČR, Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaný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

• 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ů