|
|
Hierarchické modelování plánovacích problémů
Dvořák, Tomáš ; Barták, Roman (vedoucí práce) ; Plátek, Martin (oponent)
Automatické plánování je problém nalezení sekvence akcí vedoucích z daného počátečního stavu do požadovaného cílového stavu. Existuje celá řada formálních modelů určených pro modelování plánovacích problémů. Jednou z větví je třída formálních modelů umožňujících definovat hierarchickou strukturu mezi akcemi. Tato práce navrhuje hierarchický model, nazvaný GramPlan, založený na atributových gramatikách. Ukazuje několik způsobů jak lze na GramPlan převést problém zadaný klasickým STRIPS formalismem a dokazuje korektnost těchto převodů. Práce předvádí převod workflow z FlowOpt formalismu na GramPlan a dokazuje korektnost takového převodu. Nakonec jsou navrhnuty dva způsoby jak GramPlan model verifikovat a je dokázáno, že jsou ekvivalentní a dávají stejný výsledek. Powered by TCPDF (www.tcpdf.org)
|
|
|
From textual specification to formal verification
Šimko, Viliam ; Hnětynka, Petr (vedoucí práce) ; Gruhn, Volker (oponent) ; Steinberger, Josef (oponent)
Běžný způsob popisu funkčních požadavků při vývoji softwaru je tvorba textových případů použití (use-cases). Jejich úlohou v úvodních fázích projektu je zachytit formou přirozeného jazyka způsob fungování systému z pohledu koncového uživatele. Protože jde o text psaný v přirozeném jazyce, není možné správnost textových případů použití přímo formálně ověřovat. Obdobně významným artefaktem při vývoji software je doménový model. Jde o popis nejdůležitějších konceptů a vztahů, které jsou pro vyvíjenou aplikaci důležité. Tvorba doménového modelu běžně probíhá iterativně od prvního prototypu z textu až po výsledný formální model. Tato práce se zabývá dvěma souvisejícími tématy - formální ověřování případů použití a odvozování doménového modelu z textu. První část je věnovaná metodě FOAM, která umožňuje pomocí jednoduchých anotací vložených do textu případů použití formálně ověřovat jejich správnost (model-checking). Anotace umožňují zachytit větvení kroků v případech použití a uživatel má možnost vyjádřit časové závislosti mezi různými částmi specifikace, zároveň je však zachovaná srozumitelnost původního textu. Druhá část práce popisuje tzv. Prediction Framework, který pomocí lingvistické analýzy textu a statistických klasifikátorů (log-linear Maximum Entropy models) umožňuje predikování doménového model z textu.
|
|
|
Biometrie s využitím videosekvencí sítnice
Oweis, Kamil ; Odstrčilík, Jan (oponent) ; Kolář, Radim (vedoucí práce)
Biometrické metody jsou nejmodernější způsob pro rozpoznání a ověření totožnosti osob. Jsou poměrně rychlé, bezpečné a použitelné v různých situacích. V této práci je použita sada snímků oční sítnice získaných použitím video oftalmoskopu. Snímky jsou dále upraveny pro další zpracování, nejprve převedením na černobílý binární obraz, v některých případech pak byla použita binární matice pro popis daného snímku. Poté byla navržena metoda srovnání snímků databáze s referenčním snímkem oční sítnice nazvaná metoda překrytí a posunu. Byla testována sada černobílých a poté i šedých snímků. Všechny výpočty metody byly realizovány v programu Matlab, jehož výsledkem bylo určení nejvíce shodného snímku se snímkem referenčním a vyhodnocení celkové přesnosti programu.
|
|
|
Využití výpočtového programu Impact FEM při řešení úloh mechaniky těles
Ferenc, Filip ; Kubík, Petr (oponent) ; Vosynek, Petr (vedoucí práce)
Bakalářská práce je zaměřena na výpočet základních úloh mechaniky těles s využitím programu Impact FEM. V úvodu této práce je pár základních informací o numerických výpočtech, kon-krétně o metodě konečných prvků. Dále je čtenář seznámen s programem Impact FEM. Hlavní náplní práce je verifikace geometricky jednoduchých úloh s analytickým řešením a programo-vým prostředím Ansys Workbench. Závěrem je celkové zhodnocení programu, kdy na základě dosažených výsledků je konstatováno, že program v současné době není vhodný k výpočtu úloh mechaniky těles, avšak může dobře sloužit jako výuková pomůcka.
|
|
|
Implementace přijímače a vysílače protokolu RMAP do FPGA
Walletzký, Ondřej ; Fujcik, Lukáš (oponent) ; Dvořák, Vojtěch (vedoucí práce)
Práce se zabývá návrhem a implementací řadičů protokolu RMAP používaného pro přístup do paměti mezi koncovými uzly sítě SpaceWire. V teoretické části seznamuje se sítí SpaceWire, poté podrobně popisuje protokol RMAP a sběrnicové rozhraní AMBA AHB. Praktická část se věnuje návrhu architektury řadičů zmíněného protokolu na základě standardů protokolu RMAP a sběrnice AMBA AHB. Na základě navržené architektury se pak věnuje návrhu dílčích bloků. Následně popisuje použité metody verifikace navržených řadičů a jejich testování v cílovém obvodu FPGA. Nakonec analyzuje maximální frekvenci řadičů a jejich požadavky na zdroje cílového obvodu FPGA na základě odhadů syntézy.
|
|
|
Kontrola kvality molekulárně biologických metod v transplantační medicíně
Kotrbatý, Jiří ; Kolesár, Libor (vedoucí práce) ; Schierová, Michaela (oponent)
Tato práce je zaměřena na popis zajištění kontroly kvality molekulárně-biologických metod používaných v transplantační medicíně, tedy metod HLA typizace. Kontrola kvality je součástí systému řízení kvality. Skládá se z několika prvků: validace, verifikace, interní kontrola kvality a externí hodnocení kvality. Každá zdravotnická laboratoř, včetně laboratoří zabývajících se HLA typizací, musí mít tyto prvky aplikovány do svého rutinního provozu. Validace se provádí před zavedením metody a ověřuje, zda je metoda vhodná pro zamýšlené použití. Verifikace je ověření, že validovanou metodu používáme správně v podmínkách laboratoře. Vnitřní kontrola kvality spočívá v analýze známých pozitivních a negativních vzorků a hodnotí přesnost a preciznost celého analytického procesu. V rámci externího hodnocení kvality se analyzují různé laboratoře stejný vzorek a jejich výsledky jsou vůči sobě porovnávány. Klíčová slova: HLA typizace, validace, verifikace, interní kontrola kvality, externí hodnocení kvality
|
|
|
Presenting results of software model checker via debugging interface
Kohan, Tomáš ; Šerý, Ondřej (vedoucí práce) ; Jančík, Pavel (oponent)
Název práce: Prezentace výsledků kontroly softwarového modelu skrz ladící rozhraní Autor: Tomáš Kohan Katedra: Katedra softwarového inženýrství Vedoucí diplomové práce: RNDr. Ondřej Šerý, Ph.D., Katedra distribuovaných a spolehlivých systémů Abstrakt: Cílem této práce je navrhnout a implementovat nové ladící rozhraní programu Java PathFinder. Vhodným prostředím pro toto rozhraní byl zv- olen vývojový nástroj Eclipse. Vytvořené rozhraní graficky vizualizuje výstupy programu JPF a jednotlivé detaily stavu pozastaveného virtuálního stroje (JVM), zvláště pak seznam proměnných a jejich hodnot. Za tímto účelem jsou vytvořeny dva podprojekty, a to debug4jpg a JPFDeb.core. Projekt debug4jpf kontroluje a komunikuje s instancí JPF. JPFDeb.core pak ve formě zásuvného modulu pro Eclipse poskytuje takové uživatelské rozhraní, které je podobné standardnímu rozhraní ladícího programu pro Javu. Oba projekty mezi sebou komunikují přes ad hoc komunikační protokol, který byl navržen pro tento účel. Klíčová slova: Java, verifikace, kontrola modelu, JPF, ladící rozhraní
|
|
|
Presenting results of software model checker via debugging interface
Kohan, Tomáš ; Šerý, Ondřej (vedoucí práce) ; Jančík, Pavel (oponent)
Název práce: Prezentace výsledků kontroly softwarového modelu skrz ladící rozhraní Autor: Tomáš Kohan Katedra: Katedra softwarového inženýrství Vedoucí diplomové práce: RNDr. Ondřej Šerý, Ph.D., Katedra distribuovaných a spolehlivých systémů Abstrakt: Cílem této práce je navrhnout a implementovat nové ladící rozhraní programu Java PathFinder. Vhodným prostředím pro toto rozhraní byl zv- olen vývojový nástroj Eclipse. Vytvořené rozhraní graficky vizualizuje výstupy programu JPF a jednotlivé detaily stavu pozastaveného virtuálního stroje (JVM), zvláště pak seznam proměnných a jejich hodnot. Za tímto účelem jsou vytvořeny dva podprojekty, a to debug4jpg a JPFDeb.core. Projekt de- bug4jpf kontroluje a komunikuje s instancí JPF. JPFDeb.core pak ve formě zásuvného modulu pro Eclipse poskytuje takové uživatelské rozhraní, které je podobné standardnímu rozhraní ladícího programu pro Javu. Oba projekty mezi sebou komunikují přes ad-hoc komunikační protokol, který byl navržen pro tento účel. Klíčová slova: Java, verifikace, kontrola modelu, JPF, ladící rozhraní
|
|
|
Význam numerického modelování pro řešení kontaminace podzemních vod
Havlíková, Barbora ; Datel, Josef (vedoucí práce) ; Mls, Jiří (oponent)
Práce se zabývá numerickým modelováním proudění podzemní vody a transportu kontaminantů. Tato práce je rozdělena do dvou částí. V první části jsou stručně charakterizovány a porovnány základní metody používané pro problematiku proudění podzemní vody a transportu látek. Dále jsou popsány počáteční a okrajové podmínky, které jsou nezbytnou součástí sestavování modelu. Druhá část je věnována modelům z lokality Bzenec, kde dříve docházelo k unikání chlorovaných alifatických uhlovodíků do podzemní vody. Modely byly sestaveny za účelem popisu rozsahu a šíření kontaminace a predikce dalšího vývoje znečištění.
|
|
|
User-Defined XML-to-Relational Mapping
Kohan, Tomáš ; Mlýnková, Irena (vedoucí práce) ; Nečaský, Martin (oponent)
V předložené práci studujeme možnosti mapovaní XML dat do relačních systémů. V první části popíšeme základní termíny používané v práci a následně také základní techniky pro mapování XML dat do relačních databází. V další části se budeme zabívat teoretickými metodami jako MXM a ShreX, které byly navrženy na akademické půde. V třetí části popíšeme metody mapování, které jsou použité v některých komerčních systémech jako Oracle, DB2 a MS SQL. V druhé polovině práce navrhneme novou mapovací metodu (XRM), která přinese několik nových vlastností s tím, že původní pozitivní vlastnosti zústanou zachovány. V záveru rozebereme prototypovou implmentaci navrhované mapovací metody.
|
host ::
RSS.