Scalable shared memory LTL model checking

Logo poskytovatele
Logo poskytovatele

Varování

Publikace nespadá pod Pedagogickou 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:

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