Cluster-Based I/O-Efficient LTL Model Checking

• Název česky: I/O efektivní ověřování modelu LTL s použitím výpočetních klastrů
• Autoři: BARNAT Jiří; BRIM Luboš; ŠIMEČEK Pavel
• Rok publikování: 2009
• Druh: Článek ve sborníku
• Konference: 24th IEEE/ACM International Conference on Automated Software Engineering
• Fakulta / Pracoviště MU: Fakulta informatiky
• Obor: Informatika
• Klíčová slova: parallel; I/O efficient; LTL Model Checking
• Popis: I/O efektivní algoritmy využívají rozsáhlýck kapacit externích paměťových zařízení za účelem vypořádání se s rozsáhlými datovými strukturami, které počítač není schopen uložit v rámci své operační paměti. V tomto článku ukazujeme jak I/O efektivní paralelní počítání umožňuje verifikovat systémy s až 10^10 stavy v řádu hodin.

Související projekty

• Techniky automatické verifikace a validace softwarových a hardwarových systémů
• 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
• Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů