I/O Efficient Model Checking

• Název česky: I/O-efektivní ověřování modelů
• Autoři: ŠIMEČEK Pavel
• Rok publikování: 2008
• Druh: Další prezentace na konferencích
• Fakulta / Pracoviště MU: Fakulta informatiky
• Popis: Jednou z cest, jak navýšit dostupnou paměť pro algoritmy ověřování modelů, je využití externí paměti, obzvláště hard disků. Naneštěstí, není znám žádný algoritmus založený na DFS, který by se choval efektivně v prostředí externí paměti. Ukazujeme, jak adaptovat existující algoritmy OWCTY a MAP pro detekci akceptujících cyklů založené na BFS pro I/O-efektivní použití a porovnáváme jejich I/O efektivitu a praktický výkon s existujícím přístupem k I/O-efektivnímu ověřování LTL vlastností modelů od autorů Stefana Edelkampa a Shahida Jabbara. Nové algoritmy vykazují podobnou I/O složitost s ohledem na velikost grafu, ale vyhýbají se kvadratickému nárůstu velikosti vstupního grafu. Proto je počet vykonaných I/O operací podstatně nižší a algoritmy vykazují lepší praktický výkon.

Související projekty

• Techniky automatické verifikace a validace softwarových a hardwarových systémů
• Vysoce paralelní a distribuované výpočetní systémy
• Automatizovaná verifikace softwaru