CUDA Accelerated LTL Model Checking

BARNAT, Jiří, Luboš BRIM, Milan ČEŠKA a Tomáš LAMR. CUDA Accelerated LTL Model Checking. 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.

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

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

V originále

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.

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