| |
| |
| |
|
Formal Verfication of Components in Java
Parízek, Pavel ; Plášil, František (vedoucí práce) ; Černá, Ivana (oponent) ; Pasareanu, Corina (oponent)
Formal veri cation of a hierarchical component application involves (i) checking of behavior compliance among sub-components of each composite component, and (ii) checking of implementation of each primitive component against its behavior speci cation and other properties like absence of concurrency errors. In this thesis, we focus on veri cation of primitive components implemented in Java against the properties of obeying a behavior speci cation de ned in behavior protocols (frame protocol) and absence of concurrency errors. We use the Java PathFinder model checker as a core veri cation tool. We propose a set of techniques that address the key issues of formal veri cation of real-life components in Java via model checking: support for high-level property of obeying a behavior speci cation, environment modeling and construction, and state explosion. The techniques include (1) an extension to Java PathFinder that allows checking of Java code against a frame protocol, (2) automated generation of component environment from a model in the form of a behavior protocol, (3) efficient construction of the model of environment's behavior, and (4) addressing state explosion in discovery of concurrency errors via reduction of the level of parallelism in a component environment on the basis of static analysis of Java...
|
|
Vyrovnání s nacistickou minulostí v kontextu řecko-německých vztahů
Králová, Kateřina ; Pešek, Jiří (vedoucí práce) ; Hladký, Ladislav (oponent) ; Kaiserová, Kristina (oponent)
Předložená disertační práce je historickou studií, která obeznamuje čtenáře s dosud málo probádanou problematikou poválečných řecko-německých vztahů ve stínu nacistické minulosti. Soustřeďuje se především na to, jakým způsobem se řecká společnost po druhé světové válce vypořádávala s dědictvím nacistické okupace, zvláště pak s otázku potrestání nacistických zločinů a odškodnění obětí německé okupace. Jednotlivá témata jsou přitom zkoumána v politické, socio-kulturní, ekonomické a právní rovině v kontextu studené války a po znovusjednocení Německa.
|
|
Korekce a kompenzace při měření teplot
Zábranský, Jaroslav ; Janečka, Jan (oponent) ; Vdoleček, František (vedoucí práce)
Teplota je považována za základní veličinu v oblasti průmyslového měřeni, protože na její hodnotě je závislá řada výrobních procesů a regulaci Práce je zaměřena na vlivy, působící negativně na přesnost výsledku měření teploty. Uvádí přehled těchto chyb a jejich možných kompenzací a korekcí s důrazem na časté chyby dynamické. Dynamické vlastnosti je nutné znát pro analýzu a syntézu měřících a regulačních systémů. Součástí je rovněž jednodušší model pro automatické řešení některých vybraných korekcí.
|
|
Existuje vztah mezi rozmístěním lékáren a demografickými a ekonomickými faktory?
Havlík, Karel ; Brožová, Dagmar (vedoucí práce) ; Čermáková, Klára (oponent)
Práce ověřuje existenci vztahů mezi počtem lékáren v okrese a jeho vlastnostmi. Na základě sestaveného panelu v období 2005 -- 2012 pro 73 dostupných okresů s celkovým počtem 578 pozorování jsem provedl odhad ekonometrického modelu. Z široké škály zkoumaných veličin se jako významný faktor projevila průměrná pracovní neschopnost, podíl příjemců důchodů a lékařů v populaci daného okresu, počet částí obce a hustota osídlení okresu. Dle výsledku modelu nemělo zavedení regulačního poplatku na recept statisticky významný vliv na počet lékáren, i přes znatelné snížení počtu receptů v roce 2008. Vliv mzdy nebyl podroben zkoumání z důvodu nedostupnosti dat.
|
|
Analýza hospodaření Lesů České republiky, s. p. a jeho vliv na soukromé podnikání
Prášková, Jarmila ; Vokoun, Marek (vedoucí práce) ; Šlajs, Jan (oponent)
Ve své bakalářské práci se zabývám problematikou veřejného vlastnictví lesů s důrazem na státní podnik Lesy ČR. Cílem práce je analyzovat lesnicko-dřevařský sektor a zjistit, zda veřejně vlastněné podniky dané odvětví ovlivňují, popřípadě určit jak. V teoretické části se zabývám historickým vývojem vlastnictví lesů, politickými a lesopolitickými aspekty jejich vlastnictví, mimoprodukčními funkcemi lesního hospodářství. Dále zde zkoumám postavení sektoru lesnictví v národním hospodářství a analyzuju hospodaření LČR, s. p. v období 1998-2010. Praktická část se poté snaží pomocí regresní analýzy prokázat či vyvrátit vliv veřejného vlastnictví lesů na daný sektor. Ve zkoumaném odvětví se nám podařily vypozorovat rostoucí výnosy z kapitálu a klesající výnosy z práce. Užité modely poukázaly na velkou heterogenitu dat, vliv veřejného vlastnictví se tedy prokázat nepodařilo.
|
|
Posouzení přínosu rekonverze z hlediska hodnoty církevního objektu ve vybrané lokalitě
Strnková, Markéta ; Klika, Pavel (oponent) ; Hlavinková, Vítězslava (vedoucí práce)
Diplomová práce se zabývá rekonverzí církevního objektu ve vybrané lokalitě. Na začátku jsou v práci popsány církevní objekty a jejich vliv na okolí, struktura římskokatolické církve a vývoj církevního majetku v průběhu historie. To je doplněno o základní pojmy a možné postupy oceňování kulturních památek. V praktické části se zabývám rekonverzí církevního objektu, konkrétně klášterem dominikánů ve Znojmě. Na základě analýzy Znojma a kláštera došlo k navržení možných využití kláštera. Z nich byly vybrány dvě varianty, které byly porovnány. Z těchto dvou variant byla zvolena jedna jako nejvhodnější možnost pro další využití.
|
|
Důvěra a reputace v distribuovaných systémech
Samek, Jan ; Návrat,, Pavol (oponent) ; Šafařík,, Jiří (oponent) ; Hanáček, Petr (vedoucí práce)
Tato disertační práce se zabývá problematikou modelování důvěry v distribuovaných systémech, konkrétně pak více-kontextové důvěry v distribuovaných multi-agentních systémech. V současné době existuje velké množství modelů důvěry či reputace, nicméně více-kontextová vlastnost důvěry či reputace v nich není často zohledněna. Z tohoto důvodu se práce zaměřuje především na analýzu více-kontextových modelů založených na důvěře a na jejím základě stanovuje předpoklady pro nový, vlastnost více-kontextovost plně podporující, model důvěry. Stěžejní částí práce je formální návrh nového více-kontextového modelu důvěry, který je schopen vytvářet, aktualizovat a uchovávat důvěru pro různé aspekty (kontexty) jedné entity multi-agentního systému. Důvěru lze v navrženém modelu budovat jak na základě přímých zkušeností, tak i na základě doporučení a reputace. Dalším aspektem navrženého modelu je schopnost odvozovat důvěru v různé kontexty na základě znalosti důvěry v kontexty jiné, což je zajištěno vytvořením hierarchické struktury jednotlivých kontextů jedné entity. Přínosem nového modelu je především zvýšení efektivity rozhodování agentů v rámci multi-agentního systému ve smyslu schopnosti výběru optimálního partnera pro provedení transakce. Návrh modelu byl ověřen implementací prototypu multi-agentního systému, ve kterém se agenti rozhodují a jednají na základě důvěry.
|
host ::
