J 2011

Flash memory efficient LTL model checking

EDELKAMP, Stefan, Damian SULEWSKI, Jiří BARNAT, Luboš BRIM, Pavel ŠIMEČEK et. al.

Basic information

Original name

Flash memory efficient LTL model checking

Name in Czech

Efektivní ověřování modelu s pamětmi typu flash

Authors

EDELKAMP, Stefan (276 Germany), Damian SULEWSKI (276 Germany), Jiří BARNAT (203 Czech Republic, guarantor, belonging to the institution), Luboš BRIM (203 Czech Republic, belonging to the institution) and Pavel ŠIMEČEK (203 Czech Republic, belonging to the institution)

Edition

Science of Computer Programming, Elsevier, 2011, 0167-6423

Other information

Language

English

Type of outcome

Článek v odborném periodiku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Netherlands

Confidentiality degree

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

References:

Impact factor

Impact factor: 0.622

RIV identification code

RIV/00216224:14330/11:00049402

Organization unit

Faculty of Informatics

DOI

UT WoS

000285220600006

Keywords (in Czech)

Ověřování modelu; Algoritmy pro práci s externí pamětí

Keywords in English

Model checking; External memory algorithms; Algorithm engineering

Tags

International impact, Reviewed
Změněno: 30/11/2011 11:10, prof. RNDr. Jiří Barnat, Ph.D.

Abstract

ORIG CZ

V originále

So far, large-scale LTL model checking algorithms have been designed to employ external memory optimized for magnetic disks. We propose algorithms optimized for flash memory access. In contrast to approaches relying on the delayed detection of duplicate states, in this work, we design and exploit appropriate hash functions to re-invent immediate duplicate detection.

In Czech

Metody ověřování modelu pracující s externími disky byly dosud zaměřeny poze na magnetická zařízení. V tomto článku navrhujeme algoritmy, které jsou optimlaizované pro externí disky realizované pamětí typu flash. Konkrétně oživujeme myšlenku použití hašování ve spojení s externím diskem, které bylo v předchozích pracech v kontextu ověřování modelu s využitím externích disků vyrázně potlačeno.

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