External Memory LTL Model Checking - Šimeček, Pavel (2010)
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 algor.