Diplomová práce

Trading space for time in explicit-state model checking

Bc. Pavel Mičan, učo 173327
Anotace

K snížení nároků na operační paměť v model checkingu jsme přišli s novým přístupem, který ukládá pouze určité stavy na základě jejich uspořádání. Náhodné přiřazení celočíselné hodnoty (ideálně unikátní) je dáno každému stavu a ve chvíli, kdy je zpracovávána hrana grafu je uložen pouze takový stav, který má svou přiřazenou hodnotu menší než maximum z nalezených hodnot od posledního uloženého stavu. …více

Abstract

To reduce the memory size requirements in model checking we came with an approach of storing only certain states based on their ordering. A random assignment of an integer value (ideally unique) is given to each state and while processing en edge of a graph only those states are stored which have its assigned value lower to the maximum value found since the last state had been stored. This simple solution …více

Klíčová slova
model checking verification distributed to store or not to store OWCTY Nested DFS DiVinE state space explosion
Zadání práce
The aim of the diploma thesis is to design, implement and experimentally evaluate a graph and processing independent technique that will allow DiVinE - explicit-state model checker to trade some of the memory requirements for the increased processing time. Besides the time and memory usages the experimental evaluation will also include scalability analysis on multi-core machine, aura preferably.
Administrativní informace
Práce zkontrolována:
29. 5. 2013 12:22, prof. RNDr. Jiří Barnat, Ph.D., učo 3496
Plný text práce
201,8 KB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
26. 6. 2013
Práce nebyla obhájena

Vedoucí

prof. RNDr. Jiří Barnat, Ph.D., učo 3496
KTP FI MU

Oponent

doc. Mgr. Hana Rudová, Ph.D., učo 3840
KSUZD FI MU
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Aplikovaná informatika
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.