2009
External Memory LTL Model Checking
ŠIMEČEK, PavelZá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
Vydání
Brno, 126 s. Ph.D. Thesis, 2009
Nakladatel
Faculty of Informatics, Masaryk University
Další údaje
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í
Označené pro přenos do RIV
Ano
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
Změněno: 23. 1. 2011 17:44, RNDr. Pavel Šimeček, Ph.D.
V originále
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.
Č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 |
|