Distributed LTL Model Checking with Hash Compaction

Název česky Distribuované ověřování modelů LTL za pomoci hash compaction
Autoři BARNAT Jiří — HAVLÍČEK Jan — ROČKAI Petr
Druh Článek ve sborníku
Citace BARNAT, Jiří, Jan HAVLÍČEK a Petr ROČKAI. Distributed LTL Model Checking with Hash Compaction. In Electronic Notes in Theoretical Computer Science, Volume 296. Neuveden: Elsevier Science, 2013. s. 79-93, 15 s. ISSN 1571-0661. doi:10.1016/j.entcs.2013.07.006.
Originální jazyk angličtina
Obor Informatika
WWW http://dx.doi.org/10.1016/j.entcs.2013.07.006
Doi http://dx.doi.org/10.1016/j.entcs.2013.07.006
Klíčová slova model checking; LTL; hash compaction

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í.

Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info