Disertační práce
Získaná ocenění: Ocenění děkana FI za vynikající disertační práci

External Memory LTL Model Checking

RNDr. Pavel Šimeček, učo 51636
Anotace

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ě …více

Abstract

Model checking is an increasingly popular method for formal verification of safety-critical systems. The main obstacle of this method is a state explosion problem and consequently high computational requirements of model checking algorithms. This thesis is focused on fighting state explosion by employing external memory, which can have by orders of magnitude larger capacity than internal memory. For …více

Klíčová slova
external memory I/O-efficient I/O complexity LTL model checking parallel distributed flash SSD
Administrativní informace
Práce zkontrolována:
22. 10. 2009 13:24, prof. RNDr. Luboš Brim, CSc.
Plný text práce
1 MB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
26. 1. 2010
Práce byla úspěšně obhájena

Vedoucí

prof. RNDr. Luboš Brim, CSc.
KTP FI MU

Oponenti

Priv.-Doz. Dr. Stefan Edelkamp
TZI, Universität Bremen
doc. Ing. Petr Tůma, Dr.
MFF UK v Praze
Autor posudku dosud neidentifikován.
Autor posudku dosud neidentifikován.
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Informatika (čtyřleté)
Obor

Práce na příbuzné téma

Seznam prací, které mají shodná klíčová slova.

Podobné práce

  • Přidání souboru

    Soubor nebo složku lze nahrát pomocí tlačítka Přidat.

  • Další operace se soubory

    Podrobnosti lze zjistit označením příslušného řádku.

  • Pohled pro experty

    Pro častou práci je možné zvolit režim Více možností.

  • Vyhledávání souborů

    Vyhledávaný výraz můžete zadat přímo do adresního řádku.

  • Rychlý přístup k souborům

    Pomocí funkce Nedávné je možné se rychle vrátit k právě prohlíženým souborům. Oblíbené soubory je také možné označit Hvězdičkou.