I/O Efficient Model Checking

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

Basic information

• Original name: I/O Efficient Model Checking
• Name in Czech: I/O-efektivní ověřování modelů
• Authors: ŠIMEČEK, Pavel.
• Edition: Alpine Verification Meeting 2008, 2008.

Other information

• Original language: English
• Type of outcome: Presentations at conferences
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Austria
• Confidentiality degree: is not subject to a state or trade secret
• WWW: AVM 2008 web page
• Organization unit: Faculty of Informatics
• Keywords in English: external; I/O efficient; model checking; external memory
• Tags: external, external memory, I/O efficient, Model checking
• Tags: International impact

Abstract

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.

Abstract (in Czech)

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.

Links

• GA201/06/1338, research and development project: Name: Automatizovaná verifikace softwaru

Investor: Czech Science Foundation, Automated software verification

• MSM0021622419, plan (intention): Name: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems

• 1ET408050503, research and development project: Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů

Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems