I/O Efficient Model Checking

ŠIMEČEK, Pavel. I/O Efficient Model Checking. In Alpine Verification Meeting 2008. 2008.

Základní údaje

• Originální název: I/O Efficient Model Checking
• Název česky: I/O-efektivní ověřování modelů
• Autoři: ŠIMEČEK, Pavel.
• Vydání: Alpine Verification Meeting 2008, 2008.

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Prezentace na konferencích
• Obor: 10201 Computer sciences, information science, bioinformatics
• Stát vydavatele: Rakousko
• Utajení: není předmětem státního či obchodního tajemství
• WWW: AVM 2008 web page
• Organizační jednotka: Fakulta informatiky
• Klíčová slova anglicky: external; I/O efficient; model checking; external memory
• Štítky: external, external memory, I/O efficient, Model checking
• Příznaky: Mezinárodní význam

Anotace

One way to increase a memory available to model checking algorithms is to employ the external memory, namely hard disks. Unfortunately, no DFS-based algorithm behaving efficiently in external memory environment is known. We show how to adapt an existing BFS-based accepting cycle detection algorithms OWCTY and MAP to the I/O efficient setting and compare their I/O efficiency and practical performance to the existing I/O efficient LTL model checking approach of Edelkamp and Jabbar. New algorithms exhibit similar I/O complexity with respect to the size of the graph while they avoid quadratic increase in the size of the graph. Therefore, the number of I/O operations performed is significantly lower and the algorithms exhibit better practical performance.

Anotace česky

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.

Návaznosti

• GA201/06/1338, projekt VaV: Název: Automatizovaná verifikace softwaru

Investor: Grantová agentura ČR, Automatizovaná verifikace softwaru

• MSM0021622419, záměr: Název: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy

• 1ET408050503, projekt VaV: Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů

Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů