J 2011

Flash memory efficient LTL model checking

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

Základní údaje

Originální název

Flash memory efficient LTL model checking

Název česky

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

Autoři

EDELKAMP, Stefan (276 Německo), Damian SULEWSKI (276 Německo), Jiří BARNAT (203 Česká republika, garant, domácí), Luboš BRIM (203 Česká republika, domácí) a Pavel ŠIMEČEK (203 Česká republika, domácí)

Vydání

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

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Nizozemské království

Utajení

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

Odkazy

Impakt faktor

Impact factor: 0.622

Kód RIV

RIV/00216224:14330/11:00049402

Organizační jednotka

Fakulta informatiky

DOI

UT WoS

000285220600006

Klíčová slova česky

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

Klíčová slova anglicky

Model checking; External memory algorithms; Algorithm engineering

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 30. 11. 2011 11:10, prof. RNDr. Jiří Barnat, Ph.D.

Anotace

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.

Česky

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.

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ů