Scalable shared memory LTL model checking

• 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
• 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