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

Language

English

Type of outcome

Prezentace na konferencích

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Austria

Confidentiality degree

není předmětem státního či obchodního tajemství

References:

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

V originále

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.

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