Závěrečná práce: Petr Menšík: Modelování pravděpodobnostních systémů v jazyce DiVinE
Bakalářská práce
Modelování pravděpodobnostních systémů v jazyce DiVinE
Modelling of probabilistic systems in DiVinE
Petr Menšík
Anotace
Cílem práce je formálně popsat vybrané pravděpodobnostní systémy (např. randomizované protokoly) v jazyce verifikačního nástroje DiVinE, zejména popsat modely i neformálně, uvést patřičné reference, charakterizovat specifika daného systému a shrnout použitou metodiku jako doporučení pro modelování obdobných systémů.
Abstract
The goal of this thesis is to create formal models of choice probabilistic systems (e.g. randomized protocols) in the input language of the verification tool DiVinE, especially to describe the models informally, bring appropriate references, specify properties of these systems and summarize used methodology for modelling similar systems.
Zadání práce
Cílem práce je formálně popsat vybrané pravděpodobnostní systémy (např. randomizované protokoly) v jazyce verifikačního nástroje DiVinE, zejména popsat modely i neformálně, uvést patřičné reference, charakterizovat specifika daného systému a shrnout použitou metodiku jako doporučení pro modelování odbobných systémů.
Práce zkontrolována:
11. 10. 2008 12:57, (IS automaticky)
11. 10. 2008 12:57, (IS automaticky)
Jazyk práce
čeština
Termín obhajoby
5. 2. 2008
Práce byla úspěšně obhájena
Vedoucí
prof. RNDr. Luboš Brim, CSc.
abs PřF MU
abs PřF MU
Studijní program
Aplikovaná informatika
Práce na příbuzné téma
Seznam prací, které mají shodná klíčová slova.
-
Modelování a verifikace platebního systému
Mgr. Marharyta Zhuk -
Motifs in State Spaces
RNDr. Jan Krčál, Ph.D., učo 139854 -
Návraty ke kořenům – série publicistických rozhovorů se slavnými rodáky Zlínského okresu
Mgr. Hana Bednářová, učo 181866 -
Akcelerace procesu verifikace pomocí grafické karty
Mgr. Tomáš Lamr, učo 140423 -
Vysvětlování protipříkladů v nástroji DiVinE
Mgr. Roman Plášil, učo 173458 -
Untimed LTL Model Checking of Timed Automata
Mgr. Jan Havlíček -
Modelování stateflow diagramů pro účely verifikace
Mgr. Pavla Kratochvílová -
Virtual File System in DIVINE 4
Mgr. Katarína Kejstová
Název
Vložil
Vloženo
Práva
Archiv závěrečné práce Petr Menšík FI B-AP BcAP t1sky/7
Menšík, P.
19. 12. 2007
Složky
Soubory
30. 1. 2008
-
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.