2013
Distributed LTL Model Checking with Hash Compaction
BARNAT, Jiří; Jan HAVLÍČEK a Petr ROČKAIZákladní údaje
Originální název
Distributed LTL Model Checking with Hash Compaction
Název česky
Distribuované ověřování modelů LTL za pomoci hash compaction
Autoři
BARNAT, Jiří; Jan HAVLÍČEK a Petr ROČKAI
Vydání
Neuveden, Electronic Notes in Theoretical Computer Science, Volume 296, od s. 79-93, 15 s. 2013
Nakladatel
Elsevier Science
Další údaje
Jazyk
angličtina
Typ výsledku
Stať ve sborníku
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í
Forma vydání
tištěná verze "print"
Odkazy
Označené pro přenos do RIV
Ano
Kód RIV
RIV/00216224:14330/13:00065988
Organizační jednotka
Fakulta informatiky
ISSN
UT WoS
000216919300006
Klíčová slova anglicky
model checking; LTL; hash compaction
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 28. 4. 2014 07:29, RNDr. Pavel Šmerk, Ph.D.
V originále
We extend a distributed-memory explicit-state LTL model checking algorithm (OWCTY) with hash compaction. We provide a detailed description of the improved algorithm and a correctness argument in the theoretical part of the paper. Additionally, we deliver an implementation of the algorithm as part of out parallel and distributed-memory model checker DiVinE, and use this implementation for a practical evaluation of the approach, on which we report in the experimental part of the paper.
Česky
Rozšiřujeme distribuovaný algoritmus OWCTY pro realizaci verifikační metody enumerativní ověřování modelu o možnost uchovávat navštívené stavy pouze jako jejich otisky z hashovací funkce. Podáváme detailní popis algoritmu a důkaz korektnosti. Součástí výsledku je implementace algoritmu v prostředí verifikačního nástroje DIVINE a experimentální vyhodnocení.
Návaznosti
| GAP202/11/0312, projekt VaV |
|