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. |
Další formáty:
BibTeX
LaTeX
RIS
|
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 |
Změnil | Změnil: prof. RNDr. Luboš Brim, CSc., učo 197. Změněno: 2. 2. 2011 09:38. |
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ů |
VytisknoutZobrazeno: 9. 9. 2024 20:25