Distributed LTL Model Checking with Hash Compaction

Varování

Publikace nespadá pod Ústav výpočetní techniky, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Název česky	Distribuované ověřování modelů LTL za pomoci hash compaction
Autoři	BARNAT Jiří HAVLÍČEK Jan ROČKAI Petr
Rok publikování	2013
Druh	Článek ve sborníku
Konference	Electronic Notes in Theoretical Computer Science, Volume 296
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
www	http://dx.doi.org/10.1016/j.entcs.2013.07.006
Doi	http://dx.doi.org/10.1016/j.entcs.2013.07.006
Obor	Informatika
Klíčová slova	model checking; LTL; hash compaction
Popis	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:	Software Components in Embedded Systems: Development and Verification