|
|
Hledání řídicích strategií pomocí UPPAAL STRATEGO
Hruška, Filip ; Hrubý, Martin (oponent) ; Strnadel, Josef (vedoucí práce)
Tato práce se zabývá hledáním řídicích strategií v předem vybraných problémech z různých oblastí pomocí nástroje Uppaal Stratego. Byly vybrány čtyři oblasti k řešení, jmenovitě šachy, hanojské věže, posuvné pole a kinematický problém zahrnující balíček, auto a letadlo. Pro zvolené problémy a oblasti byla navržena a vytvořena sada jim odpovídajícím modelů. U hanojských věží a posuvného pole bylo možné úspěšně vyhodnotit relevantní strategie, zvedající pravděpodobnosti úspěchu až na více než 90 %. U dalších modelů byl nalezen problém ve velikosti stavového prostoru a strategie nebylo možné vyhodnotit, protože maximální kapacita paměti, kterou nástroj využívá, nebyla dostatečná. U kinematického problému se po omezení a zjednodušení modelu podařilo strategie vyhodnotit, ovšem u šachů to nebylo možné ani po významném zjednodušení.
|
|
|
Simulace šíření infekčních onemocnění v lidské populaci
Křištof, Jiří ; Šimek, Václav (oponent) ; Strnadel, Josef (vedoucí práce)
Cílem této práce je vytvoření epidemiologického modelu pro simulaci šíření infekčního onemocnění covid-19. Vytvořený SVLIHDRS model staví na kompartmentových modelech, implementován je poté jako Markovský řetězec se spojitým časem. Pro realizaci je využit nástroj UPPAAL. Při porovnání výstupů simulace s pozorovanými daty byla určena hodnota Spearmanova koeficientu 0,8940 pro infekční jedince, pro zemřelé 0,9987, průměrné hodnoty biasu jsou poté 12510,7285, respektive 316,2697. Výsledky této práce umožňují provádět dlouhodobou předpověď vývoje epidemie infekce covid-19.
|
|
|
Analýza plánovatelnosti úloh reálného času s ohledem na nejistotu
Rosecký, Richard ; Bidlo, Michal (oponent) ; Strnadel, Josef (vedoucí práce)
Cílem této práce je navrhnout a vytvořit model systému reálného času a několika sad úloh pro tento systém, analyzovat a verifikovat vytvořený model a sady, obeznámit s problematikou systémů reálného času a plánovatelnosti úloh v těchto systémech. Pro vytvoření modelu bude použit nástroj UPPAAL a model systému bude obsahovat abstrakci úlohy, plánovače a řadících algoritmů. Ve vytvořeném modelu bude možné simulovat a verifikovat sady periodických, sporadických a aperiodických úloh v kombinaci s různými řadícími algoritmy jako FIFO, DMA, RMA, EDF nebo Round Robin.
|
|
|
Dependability Assessment Based on SMC
Gajdošík, Róbert ; Lojda, Jakub (oponent) ; Strnadel, Josef (vedoucí práce)
The aim of this thesis is assessing dependability of computerized systems using modelling and simulation. After establishing basic nomenclature, research was performed on de- pendability metrics, fault taxonomy and dependability bolstering techniques. Afterwards, analytical solutions were explored to be used as a reference point. Next, multiple simulation tools were assessed and Uppaal SMC was chosen as the most suitable tool because of it’s timed automaton framework enriched with a query language and multiple Simulation Model Checking tools. Finally, systems describing multiple relevant situations were implemented and evaluated against both themselves and the analytically computed reference point.
|
|
|
Analýza rizik spojených se samočinně řízenými vozidly
Weigel, Filip ; Šimek, Václav (oponent) ; Strnadel, Josef (vedoucí práce)
{Cílem práce bylo navrhnout a implementovat systém pro analýzu rizik v samočinně řízených vozidlech. Práce se zaměřila návrh a implementaci systému pro řešení analýzy rizik založené na modelech. Požadavkem na systém byla jeho flexibilita a robustnost. Návrh analýzy rizik byl nejprve předveden v teoretické rovině a poté implementován v modelech systémů ABS a ESP v prostředí UPPAAL. Systém byl dále podroben různým experimentům a testům pro ověření jeho funkcionality. Na implementovaném systému byly vykonané experimenty. Experimenty byly přínosné a systém pro analýzu rizik korektně vyhodnocoval scénáře selhání a adekvátně na vzrůstající riziko reagoval. Výsledky experimentů byly prezentovány na grafech s komentářem daných scénářů selhání.
|
|
|
Vyhodnocování spolehlivostních ukazatelů systémů odolných proti poruchám
Suchánek, Martin ; Šimek, Václav (oponent) ; Strnadel, Josef (vedoucí práce)
Spoľahlivosť je dôležitou súčasťou rôznych systémov. Cieľom práce je vytvorenie spoľahlivostných modelov niektorých opravovaných a neopravovaných systémov odolných proti poruchám a následné vyhodnocovanie ich spoľahlivostných ukazateľov. Na vytváranie modelov je využitý nástroj Uppaal spolu s rozšírením SMC, ktoré slúži na verifikáciu. Výsledkom práce je overenie modelov a vyhodnocovanie spoľahlivostných ukazateľov s využitím nástroja Uppaal SMC.
|
|
|
Modelování a analýza řízení samočinně parkujícího vozidla
Krucina, Marek ; Šimek, Václav (oponent) ; Strnadel, Josef (vedoucí práce)
Tato bakalářská práce se zabývá samočinně parkujícími vozidly a jejich chováním. Popisuje různé stupně automatizace parkování a s tím spojené technologie. Zabývá se kinematickým modelem vozidla a různými způsoby reprezentace pohybu. Shrnuje základní modelovací nástroje a věnuje se především nástroji UPPAAL SMC, ve kterém je následně vytvořen model samočinně parkujícího vozidla a jeho okolí, jehož implementace je v práci popsána. V závěru práce je vytvořený model podroben analýze pomocí metody statistického ověřování modelu a následně je zkoumán vliv hustoty provozu.
|
|
|
Překlad XTR výstupu nástroje UPPAAL do uživatelsky přívětivé reprezentace
Mazánek, Antonín ; Mrázek, Vojtěch (oponent) ; Strnadel, Josef (vedoucí práce)
Diplomová práce seznamuje s nástrojem Uppaal. Popisuje principy a možnosti modelování a analýzy systémů pomocí tohoto nástroje. Dále se blíže zabývá formáty souborů, které nástroj Uppaal používá. Strukturou souboru XML, sloužící pro uložení vytvořených systémů, formátem XTR, který nástroj používá k ukládání simulačních běhů, a formátem IF, který je nutný k porozumění obsahu souboru ve formátu XTR. V textu je zmíněna i dostupná programová podpora pro práci s těmito formáty. Další částí, kterou se tato diplomová práce zabývá, já návrh uživatelsky přívětivé reprezentace simulačních běhů spolu s návrhem a implementací aplikace, která provádí překlad simulačních běhů nástroje Uppaal do navržené reprezentace. Na konci práce je zmíněno možné pokračování v projektu spolu s hodnocením navržené reprezentace a aplikace pro překlad.
|
|
|
Výpočetní model a analýza systému adaptivních semaforů
Terbr, Filip ; Šimek, Václav (oponent) ; Strnadel, Josef (vedoucí práce)
Bakalářská práce se věnuje tématu adaptivních křižovatek a studiem jejich vlivu na plynulost provozu a jiné. V práci je obsažen rozbor aktuálně používaných dopravních detektorů, rozbor hlavních problémů klasických křižovatek a možnosti jejich řešení, následně návrh modelu, popis realizace a testování vytvořeného modelu. Výsledný model je vytvořen v softwaru UPPAAL SMC a jedná se o systém navzájem komunikujících časovaných automatů. Testování probíhá porovnáváním výsledků testů klasických semaforů s výsledky adaptivních semaforů.
|
|
|
Vliv ESP/ESC na chování vozidla
Weigel, Filip ; Mrázek, Vojtěch (oponent) ; Strnadel, Josef (vedoucí práce)
Práce se zabývá aktivním prvkem bezpečnosti vozidel - ESP. Systém ESP velmi významně pomáhá se stabilizací vozidla při zatáčení. Práce rozebírá modelování, princip fungování brzd, popis podřízených systémů - ABS a ASR, fyzikální jevy a síly, vzorový příklad, rozbor problému, návrh modelu, implementaci modelu a vyhodnocení experimentů s modelem v prostředí UPPAAL. Cílem práce je prokázat, že systém ESP pomáhá stabilizovat vozidlo při zatáčení pomocí simulačního modelu vozidla. Výsledky jsou prezentány v přehledných grafech. Z grafů lze analyzovat chování vozidla s ESP a bez ESP.
|
host ::
RSS.