EDELKAMP, Stefan, Damian SULEWSKI, Jiří BARNAT, Luboš BRIM a Pavel ŠIMEČEK. Flash memory efficient LTL model checking. Science of Computer Programming, Elsevier, 2011, roč. 76, č. 2, s. 136--157. ISSN 0167-6423. doi:10.1016/j.scico.2010.03.005.
Další formáty:   BibTeX LaTeX RIS
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
Originální jazyk angličtina
Typ výsledku Článek v odborném periodiku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Nizozemsko
Utajení není předmětem státního či obchodního tajemství
WWW URL
Impakt faktor Impact factor: 0.622
Kód RIV RIV/00216224:14330/11:00049402
Organizační jednotka Fakulta informatiky
Doi http://dx.doi.org/10.1016/j.scico.2010.03.005
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ěnil Změnil: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Změněno: 30. 11. 2011 11:10.
Anotace
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.
Anotace č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 VaVNázev: Automatizovaná verifikace softwaru
Investor: Grantová agentura ČR, Standardní projekty
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumné záměry
1ET408050503, projekt VaVNázev: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Akademie věd ČR, Informační společnost (Národní program výzkumu)
VytisknoutZobrazeno: 26. 1. 2020 03:40