DiVinE Multi-Core -- A Parallel LTL Model-Checker
BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. DiVinE Multi-Core -- A Parallel LTL Model-Checker. In Automated Technology for Verification and Analysis. Berlin / Heidelberg: Springer, 2008, s. 234-239. ISBN 978-3-540-88386-9. |
Další formáty:
BibTeX
LaTeX
RIS
|
Základní údaje | |
---|---|
Originální název | DiVinE Multi-Core -- A Parallel LTL Model-Checker |
Název česky | DiVinE Multi-Core -- Paralelní nástroj pro ověřování modelu LTL |
Autoři | BARNAT, Jiří (203 Česká republika, garant), Luboš BRIM (203 Česká republika) a Petr ROČKAI (203 Česká republika). |
Vydání | Berlin / Heidelberg, Automated Technology for Verification and Analysis, od s. 234-239, 6 s. 2008. |
Nakladatel | Springer |
Další údaje | |
---|---|
Originální jazyk | angličtina |
Typ výsledku | Stať ve sborníku |
Obor | 10201 Computer sciences, information science, bioinformatics |
Stát vydavatele | Korejská republika |
Utajení | není předmětem státního či obchodního tajemství |
Impakt faktor | Impact factor: 0.402 v roce 2005 |
Kód RIV | RIV/00216224:14330/08:00024321 |
Organizační jednotka | Fakulta informatiky |
ISBN | 978-3-540-88386-9 |
ISSN | 0302-9743 |
UT WoS | 000261873000019 |
Klíčová slova anglicky | LTL Model Checking; Parallel; Tool |
Štítky | LTL model checking, parallel, tool |
Příznaky | Mezinárodní význam, Recenzováno |
Změnil | Změnil: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Změněno: 30. 3. 2010 09:14. |
Anotace |
---|
We present a tool for parallel shared-memory enumerative LTL model-checking and reachability analysis. The tool is based on distributed-memory algorithms reimplemented specifically for multi-core and multi-cpu environments using shared memory. We show how the parallel algorithms allow the tool to exploit the power of contemporary hardware, which is based on increasing number of CPU cores in a single system, as opposed to increasing speed of a single CPU core. |
Anotace česky |
---|
V tomto článku prezentujeme nástro pro paralelní ověřování modelu v paralelním prostředí se sdílenou pamětí. Nástroj je založen na algoritmech použivaných v prostředí s distribuovanou pamětí, ale tyto efektivně reimplementuje v prostředí se sdílenou pamětí. Smyslem nástroje je demonstrovat způsob, kterým lze zcela využít sílu soudobého HW, jmenovitě nových více=jádrových procesorů. |
Návaznosti | |
---|---|
GA201/06/1338, projekt VaV | Název: Automatizovaná verifikace softwaru |
Investor: Grantová agentura ČR, Automatizovaná verifikace softwaru | |
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 |
VytisknoutZobrazeno: 23. 9. 2024 09:36