External Memory LTL Model Checking
| Název česky | Ověřování modelů LTL s použitím externí paměti |
|---|---|
| Autoři | |
| Rok publikování | 2009 |
| Druh | Účelové publikace |
| Fakulta / Pracoviště MU | |
| Citace | |
| Popis | (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í. |
| Související projekty: |