|
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...
|
|
Kontrola, regulace a úprava jaderného zbrojení
Bříza, Vlastislav ; Ondřej, Jan (vedoucí práce) ; Šturma, Pavel (oponent) ; Kozák, Kryštof (oponent)
V rámci širšího pojetí kontroly jaderného zbrojení a jaderného odzbrojení se predkládaná práce soustredí zejména na otázky spojené se zákazem jaderných zkoušek, nešírením jaderných zbraní a vytvárením zón bez jaderných zbraní, které jsou rozebrány detailne. Další zmínené aspekty, konkrétne snižování poctu jaderných zbraní, problematika potenciálních nosicu jaderných zbraní ci problematika kontroly štepného materiálu jsou zmíneny pouze okrajove ve vazbe na tri hlavní oblasti bádání. Vzhledem k roli, kterou pri snaze o kontrolu jaderného zbrojení a o jaderné odzbrojení hrály mezinárodní organizace v cele s OSN a Mezinárodní agenturou pro atomovou energii IAEA, je pozornost venována i temto organizacím, resp. institucím.
|
|
Odsíření spalin fluidního kotle.
Miklík, Tomáš ; Slezák, Pavel (oponent) ; Skála, Zdeněk (vedoucí práce)
Cílem práce je navrhnout odsiřovací zařízení fluidního kotle. Ve fluidním kotli se spaluje palivo s extrémně vysokým obsahem síry a spaliny se v něm neodsíří na požadovanou úroveň, proto se musí přistavět odsiřovací zařízení. Práce je rozdělena na teoretickou a praktickou část. V teoretické části jsou uvedeny emisní limity oxidu siřičitého, zpracovány možné odsiřovací metody a popsány sorbenty vhodné pro odsiřování. V praktické části je vybrána suchá odsiřovací metoda s fluidním reaktorem, do kterého se bude dávkovat suchý sorbent na bázi vápenného hydrátu. Pro požadované hodnoty je navrženo celé odsiřovací zařízení včetně látkových filtrů, všech potřebných sil a větších komponent. Jedná se o projekční návrh s dispozičním řešením a prostorovým modelem.
|
|
Effect of low doses of herbicide paraquat on antioxidant defense in Drosophila
SÁBOVÁ, Michala
Disruption of cell equilibrium between production of free radicals and antioxidant defence is named oxidative stress. The main component of antioxidant mechanism is activity of antioxidant enzymes, which include superoxide dismutase (SOD) and catalase. In this study we evaluated the effect of herbicide paraquat on response of SOD and catalase, their transcription level and locomotion activity in Drosophila melanogaster. We exposed the flies to a wide range of paraquat concentration. Our results revealed that transcript and enzymatic levels of both SOD and catalase have a similar biphasic dose response with the peaks at 2,5 ?M paraquat concentration, resembling hormetic effect. Then, males were more sensitive than females. However, females had an increased locomotion activity. We found that paraquat susceptibility is increased in males and mating flies. Therefore, this study supports hypothesis of stress sensitivity elevation as a physiological cost of reproduction.
|
| |
|
Rurální pohraničí Česka
Vaishar, Antonín
Pro analýzu českého pohraničí bylo vyčleněno 110 pohraničních regionů, tvořených spádovými obvody pověřených obecních úřadů. Byla konstatována následující fakta: mírně příznivější demografická situace pohraničí (zvláště rurálního), výrazně horší vzdělanostní struktura, vyšší nezaměstnanost, která nicméně souvisí především se strukturální přestavbou ekonomiky, nedostatečná infrastruktura. Budoucnost rurálního pohraničí je spatřována spíše v udržitelném osídlení než v ekonomickém rozvoji. Hlavní překážkou rozvoje a přeshraniční spolupráce se zdá být kvalifikační struktura populace. Zatímco sociální kontakty se začaly rozvíjet, zatímco ekonomická spolupráce je na samém začátku. Dašlí výzkum bude zaměřen na mikroregiony velmi malých středisek, která mohou být považována za nejproblematičtější.
|
|
Taxonomie cloud služeb
Staňková, Zuzana ; Karkošková, Soňa (vedoucí práce) ; Vencovský, Filip (oponent)
Tato bakalářská práce s názvem "Taxonomie cloud služeb" se zabývá popisem a kategorizací služeb v oblasti cloud computingu. Má za cíl teoreticky popsat a přiblížit celý tento model poskytování ICT služeb, zanalyzovat dva přední poskytovatele cloudových služeb a přinést nový pohled na jeho taxonomii. V teoretické části práce je vymezen pojem cloud computing, jeho definice a stručně popsána historie. Dále je věnována pozornost jednotlivým komponentám, charakteristikám či infrastruktuře. Jsou vymezeny základní teoretické modely členění cloud computingu a nakonec je věnováno několik kapitol bezpečnosti celé technologie, jejím výhodám a nevýhodám a také otázce legislativy. Praktická část práce se potom zabývá v první řadě analýzou dvou předních poskytovatelů cloudových služeb, přičemž největší pozornost je věnována zkoumání charakteristik, které poskytovatelé u svých produktů uvádí. Následně je vytvořen model pro zobecněnou víceúrovňovou taxonomii služeb v oblasti cloud computingu na základě zkoumaných charakteristik. V závěru praktické části je uplatnění taxonomie demonstrováno na jednoduchém aplikačním příkladu a celá práce je shrnuta.
|
|
Model měření výšky hladiny
Pavliš, Michal ; Zuth, Daniel (oponent) ; Vdoleček, František (vedoucí práce)
Tato diplomová práce se zabývá v teoretické části popsáním a vysvětlením principů a možností, jak měřit výšku hladiny. Jsou zde objasněny jednotlivé druhy a typy snímačů k měření výšky hladiny. Dále je popsán software a hardware, který se používá k měření, či ovládání mnohých systémů a soustav. Praktická část práce spočívá v návrhu a vlastní realizaci modelu měření výšky hladiny včetně jeho řízení. V neposlední řadě také vytvoření jednak návodu na obsluhu laboratorního pracoviště, a dále vytvoření příslušného měřícího a ovládacího software v systému Control Web 6. Práce se především zaměřuje na modelové přiblížení této problematiky potřebám pro účely laboratorní výuky.
|
|
Aromatické látky v koření
SVOBODOVÁ, Hana
Cílem diplomové práce bylo vytvořit výukový program na principech badatelsky orientovaného vyučování na téma ,,Aromatické látky v koření?, program použít ve výuce a ověřit úroveň žákovských znalostí získaných absolvovanou výukou. Výukový program byl aplikován u dvou skupin respondentů, z nichž jedna absolvovala výuku formou badatelsky orientovaného vyučování s využitím vytvořeného pracovního listu a druhá skupina formou frontální výuky. U těchto skupin byl proveden srovnávací průzkum formou didaktického testu. Statisticky průkazný rozdíl zjištěných výsledků byl ověřován Studentovým t-testem na hladině významnosti 0,05. V rámci statistického zhodnocení výsledků obou testovaných skupin byl zjišťován vliv badatelsky orientovaného vyučování na úroveň žákovských poznatků.
|
|
Hierarchické řízení vícesměrového robota
Pazdera, Miroslav ; Holý, Miroslav (oponent) ; Lacko, Branislav (vedoucí práce)
Náplní této diplomové práce je návrh řídícího systému pro mobilní robotický podvozek pohybující se po horizontální matici kuličkových elementů. Součástí práce je analýza pohybů podvozku a definování instrukcí pro řídící úroveň. Instrukce řídící úrovně jsou zpracovány ve vytvořeném simulačním programu. Součástí práce je návrh elektronických součástek a požadavků na elektroniku řídících subsystémů.
|
host ::
