|
| |
|
|
Analýza dopadu strategií řešení problémů pomocí UPPAAL STRATEGO
Karásek, Filip ; Žádník, Martin (oponent) ; Strnadel, Josef (vedoucí práce)
Tato práce analyzuje a řeší dopad strategií vytvořených pomocí Uppaal Stratego. V této práci je ukázána implementace čtyř problémů, čítač, bludiště, bitmapa a křižovatka. Nad těmito modely jsou prováděny experimenty a vytvářeny strategie. Pro první tři problémy byly nalezeny strategie s pozitivním dopadem na daný systém. Pro poslední model křižovatky, se nepodařilo nalézt takovou strategii, která by prokazatelně vylepšila systém. Neprokazatelně, protože se nepodařilo nalézt strategii pro model s vyšším počtem vozidel v křižovatce a to z důvodu omezení Uppaal Stratego a komplexnosti modelu.
|
|
|
Statistické ověřování modelů přibližných výpočetních systémů
Blažek, Michal ; Sekanina, Lukáš (oponent) ; Strnadel, Josef (vedoucí práce)
Tato bakalářská práce se zaměřuje na statistické ověřování modelů přibližných násobiček. Zejména se zabývá srovnáním vlastností násobiček při generování jejich vstupních hodnot podle různých pravděpodobnostních rozdělení. Součástí práce je převod modelů násobiček z knihovny EvoApproxLib do modelů v prostředí UPPAAL. Vytvořené modely jsou poté simulovány s ohledem na vybrané hodnotící metriky, jako např. pravděpodobnost chyby, průměrná absolutní chyba aj. Ze získaných výsledků lze usuzovat, že použitím vhodné aproximační násobičky pro provádění výpočtů v rámci konkrétní aplikace je možné docílit menší chyby ve výpočtech. Výsledky by proto mohly mít další uplatnění v oblasti přibližných výpočetních systémů.
|
|
|
Analýza vlastností vlakového provozu řízeného pomocí ERTMS/ETCS
Ondroušek, Adam ; Šimek, Václav (oponent) ; Strnadel, Josef (vedoucí práce)
Cílem této práce je analýza vlakového provozu řízeného ERTMS/ETCS především na území České republiky. Byl vytvořen model pomocí softwaru Uppaal, který simuluje vlakový provoz. Následně byl navržen scénář, který podstatně zvýšil efektivitu modelované tratě. Tento scénář byl verifikován pomocí simulačních a pravděpodobnostních dotazů Uppaal SMC. Povedlo se dosáhnout příznivých výsledků zdvojnásobením intervalů osobní dopravy ve frekventovaných hodinách a doplnit nákladní vlakové jednotky do provozu v této době s minimální časovou prodlevou při zachování bezpečnosti provozu. Model je koncipován tak, aby dokázal simulovat libovolnou vlakovou jednotku a traťový úsek a mohl by tedy sloužit jako nástroj pro plánování a analýzu vlakové dopravy po zavedení ERTMS/ETCS.
|
|
|
Multi-Platform Tool for Generation of Technical Documentation from XML
Jánošíková, Simona ; Setinský, Jiří (oponent) ; Strnadel, Josef (vedoucí práce)
This bachelor's thesis deals with the challenge in the field of technical documentation of development environments and explores the possibilities of automated generation of documentation from structured XML data. The problem lies in the need for efficient creation and maintenance of technical project documentation through an automated process. The goal of the work is to design, implement and evaluate a multi-platform tool that will be able to generate technical documentation from XML inputs with an emphasis on practical usability in real projects. The work is useful for developers who are involved in the creation and maintenance of technical documentation of development environments. It provides a specific tool that can streamline the documentation generation process and improve the readability of documentation within projects using the XML format for storing information.
|
|
|
Analýza plánovatelnosti úloh reálného času s ohledem na nejistotu
Čus, Samuel ; Šimek, Václav (oponent) ; Strnadel, Josef (vedoucí práce)
Cílem této bakalářské práce je seznámení se se systémy pracujícími v reálném čase, nejistotami a plánovacími mechanismy, souvisejícími s těmito systémy, statistickým ověřováním modelů, dále je to návrh a implementace přístupu k analýze plánovatelnosti s ohledem na nejistoty, vytvoření vhodných sad úloh reálného času a ověření jejich plánovatelnosti. Zaměřil jsem se na nejistoty způsobené přerušením systému a nedeterministickými parametry úloh. Zadaný problém jsem řešil vytvořením sad úloh, zavedením nejistot do systému a analýzou plánovatelnosti úloh. Modelování systému a jeho analýza bylo provedeno v nástroji UPPAAL SMC pro porovnaní také v nástroji Cheddar u vybraných sad úloh.
|
|
|
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.
|
|
|
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.
|
|
|
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.
|
|
|
Model úloh s omezeními a mechanismů jejich plánování v UPPAAL SMC
Palúch, Filip ; Podivínský, Jakub (oponent) ; Strnadel, Josef (vedoucí práce)
Cieľom je vytvorenie prehľadu mechanizmov plánovania úloh v jednoprocesorovom prostredí. Použitím týchto mechanizmov sú navrhnuté a implementované jednotlivé modely v nástroji UPPAAL, na ktorý sa táto práca orientuje. Výsledkom práce je overenie validity a vlastností mechanizmov získaných na základe implementovania modelov. Na porovnávanie výsledkov z nástroja UPPAAL sú využíté nástroje TimesTool a Cheddar.
|
host ::
RSS.