Flash memory efficient LTL model checking

• Název česky: Efektivní ověřování modelu s pamětmi typu flash
• Autoři: EDELKAMP Stefan; SULEWSKI Damian; BARNAT Jiří; BRIM Luboš; ŠIMEČEK Pavel
• Rok publikování: 2011
• Druh: Článek v odborném periodiku
• Časopis / Zdroj: Science of Computer Programming
• Fakulta / Pracoviště MU: Fakulta informatiky
• Citace: 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. Dostupné z: https://dx.doi.org/10.1016/j.scico.2010.03.005.
• www: http://dx.doi.org/10.1016/j.scico.2010.03.005
• Doi: http://dx.doi.org/10.1016/j.scico.2010.03.005
• Obor: Informatika
• Klíčová slova: Model checking; External memory algorithms; Algorithm engineering
• Popis: 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.

Související projekty

• Techniky automatické verifikace a validace softwarových a hardwarových systémů
• Vysoce paralelní a distribuované výpočetní systémy
• Automatizovaná verifikace softwaru