Scalable shared memory LTL model checking

Varování

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

Autoři	BARNAT Jiří BRIM Luboš ROČKAI Petr
Rok publikování	2010
Druh	Článek v odborném periodiku
Časopis / Zdroj	International Journal on Software Tools for Technology Transfer (STTT)
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
www	http://dx.doi.org/10.1007/s10009-010-0136-z
Doi	http://dx.doi.org/10.1007/s10009-010-0136-z
Obor	Informatika
Klíčová slova	LTL Model Cecking; Parallel; Shared-Memory
Popis	Nedávný vývoj v oblasti počítačového HW vedl k masovému rozšíření vícekórových výpočetních systémů. Tyto systémy umožňují akceleraci různých úloh paralelizací. V článku je popsán návrh paralelního nástroje pro LTL ověřování modelu. Paralelní škálovatelnost nástroje je umocněna nově navrhnutými implementačními technikami. Nástroj byl pro účely článku experimentálně evaluován na několika modelech, zpráva o této evaluaci je součástí článku. Nástroj vykazuje vzhledem k své sekvenční verzi významné zrychlení procesu verifikace.
Související projekty:	Techniky automatické verifikace a validace softwarových a hardwarových systémů Institut Teoretické Informatiky Vysoce paralelní a distribuované výpočetní systémy Verifikace a analýza velmi velkých počítačových systémů Automatizovaná formální verifikace s využitím soudobého hardware Rozsáhlé výpočetní systémy: modely, aplikace a verifikace