CUDA Accelerated LTL Model Checking

BARNAT, Jiří, Luboš BRIM, Milan ČEŠKA a Tomáš LAMR. CUDA Accelerated LTL Model Checking. Online. In Proceedings of the 15th International Conference on Parallel and Distributed Systems. Neuveden: Roy Sterritt, 2009. s. 34-41. ISBN 978-0-7695-3900-3. [citováno 2024-04-24]

Základní údaje

• Originální název: CUDA Accelerated LTL Model Checking
• Název česky: CUDA akcelerované LTL ověřování modelů
• Autoři: BARNAT, Jiří (203 Česká republika, garant, domácí), Luboš BRIM (203 Česká republika, domácí), Milan ČEŠKA (203 Česká republika, domácí) a Tomáš LAMR (203 Česká republika, domácí)
• Vydání: Neuveden, Proceedings of the 15th International Conference on Parallel and Distributed Systems, od s. 34-41, 8 s. 2009.
• Nakladatel: Roy Sterritt

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Stať ve sborníku
• Obor: 10201 Computer sciences, information science, bioinformatics
• Stát vydavatele: Spojené státy
• Utajení: není předmětem státního či obchodního tajemství
• Kód RIV: RIV/00216224:14330/09:00028692
• Organizační jednotka: Fakulta informatiky
• ISBN: 978-0-7695-3900-3
• Klíčová slova česky: ověřování modelů; lineární temporální logika; CUDA
• Klíčová slova anglicky: Model Checking; Linear Temporal Logic; CUDA
• Příznaky: Mezinárodní význam, Recenzováno

Anotace

Recent technological developments made available various many-core hardware platforms. For example, a SIMD-like hardware architecture became easily accessible for many users who have their computers equipped with modern NVIDIA GPU cards with CUDA technology. In this paper we redesign the maximal accepting predecessors algorithm [7] for LTL model checking in terms of matrix-vector product in order to accelerate LTL model checking on many-core GPU platforms. Our experiments demonstrate that using the NVIDIA CUDA technology results in a significant speedup of verification process.

Anotace česky

Současný technologický vývoj zpřístupnil různé mnohajádrové architektury. Například SIMD architektury se staly snadno dostupné pro mnoho uživatelů, kteří mají počítače vybavené moderními NVIDIA GPU kartami s CUDA technologií. V tomto článku jsme modifikovali algoritmus maximálního akceptujícího předchůdce [7] používaného pro LTL ověřování modelů pomocí násobení matice vektorem. Tato modifikace umožnila akceleraci LTL ověřování modelů na mnohajádrových GPU architekturách. Naše experimenty demonstrovaly, že použití NVIDIA CUDA technologie vedlo k výraznému zrychlení verifikačního procesu.

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ů

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