Scalable shared memory LTL model checking

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, 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