External Memory LTL Model Checking

ŠIMEČEK, Pavel. External Memory LTL Model Checking. Brno: Faculty of Informatics, Masaryk University, 2009, 126 s. Ph.D. Thesis.

Základní údaje

• Originální název: External Memory LTL Model Checking
• Název česky: Ověřování modelů LTL s použitím externí paměti
• Autoři: ŠIMEČEK, Pavel (203 Česká republika, garant, domácí).
• Vydání: Brno, 126 s. Ph.D. Thesis, 2009.
• Nakladatel: Faculty of Informatics, Masaryk University

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Účelové publikace
• Obor: 10201 Computer sciences, information science, bioinformatics
• Stát vydavatele: Česká republika
• Utajení: není předmětem státního či obchodního tajemství
• Kód RIV: RIV/00216224:14330/09:00047049
• Organizační jednotka: Fakulta informatiky
• Klíčová slova česky: LTL ověřování modelů I/O-efektivní externí paměť flash SSD
• Klíčová slova anglicky: LTL model checking I/O-efficient external memory flash SSD

Anotace

Model checking is an increasingly popular method for formal verification of safety-critical systems. This thesis is focused on fighting state explosion (the well-known problem in model checking) by employing external memory, which can have by orders of magnitude larger capacity than internal memory. For computations, probably the most proper external memory device is hard disk. It has a sufficient speed and capacity for a low price. As a drawback, hard disks suffer from long access times, which means than data must be read by blocks in order to preserve a sufficient transfer rate. Therefore, model checking algorithms must be re-designed to behave efficiently w.r.t. the number of performed I/O operations when a substantial part of a state space is stored on disk. The thesis offers I/O-efficient solutions to the two well-known model checking problems --- reachability analysis and LTL model checking. All newly designed algorithms have been implemented, thoroughly experimentally evaluated and analysed.

Anotace česky

(plná verze, anglicky je zkrácená): Ověřování modelů je stále oblíbenější metodou formální verifikace systémů s vysokými požadavky na bezpečnost. Hlavní překážkou této metody je problém stavové exploze a následná vysoká hardwarová náročnost algoritmů pro ověřování modelů. Tato práce je zaměřena na boj se stavovou explozí za pomoci zapojení vnější paměti, která může mít řádově větší kapacitu než vnitřní paměť. Pro výpočty je pravděpodobně nejvhodnějším typem vnější paměti hard disk. Má dostatečnou rychlost a kapacitu za nízkou cenu. Nevýhoda hard disků je, že mají dlouhou přístupovou dobu, což znamená, že data musí být čtena po blocích, aby byla zachována dostatečná přenosová rychlost. Z těchto důvodů algoritmy pro ověřování modelů musí být znovu navrženy tak, aby se chovaly efektivně vzhledem k počtu vykonaných vstupně-výstupních operací, když je podstatná část stavového prostoru uložena na disku. Tato práce přispívá několika cestami k vývoji takových algoritmů. Za prvé, poskytuje celistvý přehled současného stavu algoritmů pro ověřování modelů používajících vnější paměť. Za druhé, nabízí vstup-výstupně efektivní řešení dvou dobře známých problémů ověřování modelů --- analýzy dosažitelnosti a ověřování LTL vlastností modelů. Za třetí, zkoumá polo-vnější přístup k ověřování modelů, který povoluje uložit konstantní počet bitů na stav ve vnitřní paměti, aby se ušetřily nákladné vstupně-výstupní operace. V tomto uspořádání pak práce představuje nový polo-vnější algoritmus pro ověřování LTL vlastností modelů, který využívá perfektního hašování pro detekci duplikátů již navštívených stavů. Nakonec práce zkoumá složitější hardwarové sestavy --- architektury souběžných systémů a tzv. solid state disky --- za účelem urychlení procesu ověřování modelů. U všech nově navržených algoritmů je analyzována jejich vstupně-výstupní složitost, která vyjadřuje počet vykonaných vstupně-výstupních operací.

Návaznosti

• 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