|
Analysis and Testing of Concurrent Programs
Letko, Zdeněk ; Lourenco, Joao (oponent) ; Sekanina, Lukáš (oponent) ; Vojnar, Tomáš (vedoucí práce)
The thesis starts by providing a taxonomy of concurrency-related errors and an overview of their dynamic detection. Then, concurrency coverage metrics which measure how well the synchronisation and concurrency-related behaviour of tested programs has been examined are proposed together with a~methodology for deriving such metrics. The proposed metrics are especially suitable for saturation-based and search-based testing. Next, a novel coverage-based noise injection techniques that maximise the number of interleavings witnessed during testing are proposed. A comparison of various existing noise injection heuristics and the newly proposed heuristics on a set of benchmarks is provided, showing that the proposed techniques win over the existing ones in some cases. Finally, a novel use of stochastic optimisation algorithms in the area of concurrency testing is proposed in the form of their application for finding suitable combinations of values of the many parameters of tests and the noise injection techniques. The approach has been implemented in a prototype way and tested on a set of benchmark programs, showing its potential to significantly improve the testing process.
|
|
Relational Verification of Programs with Integer Data
Konečný, Filip ; Bouajjani, Ahmed (oponent) ; Jančar, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
This work presents novel methods for verification of reachability and termination properties of programs that manipulate unbounded integer data. Most of these methods are based on acceleration techniques which compute transitive closures of program loops. We first present an algorithm that accelerates several classes of integer relations and show that the new method performs up to four orders of magnitude better than the previous ones. On the theoretical side, our framework provides a common solution to the acceleration problem by proving that the considered classes of relations are periodic. Subsequently, we introduce a semi-algorithmic reachability analysis technique that tracks relations between variables of integer programs and applies the proposed acceleration algorithm to compute summaries of procedures in a modular way. Next, we present an alternative approach to reachability analysis that integrates predicate abstraction with our acceleration techniques to increase the likelihood of convergence of the algorithm. We evaluate these algorithms and show that they can handle a number of complex integer programs where previous approaches failed. Finally, we study the termination problem for several classes of program loops and show that it is decidable. Moreover, for some of these classes, we design a polynomial time algorithm that computes the exact set of program configurations from which nonterminating runs exist. We further integrate this algorithm into a semi-algorithmic method that analyzes termination of integer programs, and show that the resulting technique can verify termination properties of several non-trivial integer programs.
|
|
Acceleration Methods for Evolutionary Design of Digital Circuits
Vašíček, Zdeněk ; Miller, Julian (oponent) ; Zelinka,, Ivan (oponent) ; Sekanina, Lukáš (vedoucí práce)
Although many examples showing the merits of evolutionary design over conventional design techniques utilized in the field of digital circuits design have been published, the evolutionary approaches are usually hardly applicable in practice due to the various so-called scalability problems. The scalability problem represents a general problem that refers to a situation in which the evolutionary algorithm is able to provide a solution to a small problem instances only. For example, the scalability of evaluation of a candidate digital circuit represents a serious issue because the time needed to evaluate a candidate solution grows exponentially with the increasing number of primary inputs. In this thesis, the scalability problem of evaluation of a candidate digital circuit is addressed. Three different approaches to overcoming this problem are proposed. Our goal is to demonstrate that the evolutionary design approach can produce interesting and human competitive solutions when the problem of scalability is reduced and thus a sufficient number of generations can be utilized. In order to increase the performance of the evolutionary design of image filters, a domain specific FPGA-based accelerator has been designed. The evolutionary design of image filters is a kind of regression problem which requires to evaluate a large number of training vectors as well as generations in order to find a satisfactory solution. By means of the proposed FPGA accelerator, very efficient nonlinear image filters have been discovered. One of the discovered implementations of an impulse noise filter consisting of four evolutionary designed filters is protected by the Czech utility model. A different approach has been introduced in the area of logic synthesis. A method combining formal verification techniques with evolutionary design that allows a significant acceleration of the fitness evaluation procedure was proposed. The proposed system can produce complex and simultaneously innovative designs, overcoming thus the major bottleneck of the evolutionary synthesis at gate level. The proposed method has been evaluated using a set of benchmark circuits and compared with conventional academia as well as commercial synthesis tools. In comparison with the conventional synthesis tools, the average improvement in terms of the number of gates provided by our system is approximately 25%. Finally, the problem of the multiple constant multiplier design, which belongs to the class of problems where a candidate solution can be perfectly evaluated in a short time, has been investigated. We have demonstrated that there exists a class of circuits that can be evaluated efficiently if a domain knowledge is utilized (in this case the linearity of components).
|
|
Simulace a protiřetězce pro efektivní práci s konečnými automaty
Holík, Lukáš ; Černá, Ivana (oponent) ; Jančar, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis is focused on techniques for finite automata and their use in practice, with the main emphasis on nondeterministic tree automata. This concerns namely techniques for size reduction and language inclusion testing, which are two problems that are crucial for many applications of tree automata. For size reduction of tree automata, we adapt the simulation quotient technique that is well established for finite word automata. We give efficient algorithms for computing tree automata simulations and we also introduce a new type of relation that arises from a combination of tree automata downward and upward simulation and that is very well suited for quotienting. The combination principle is relevant also for word automata. We then generalise the so called antichain universality and language inclusion checking technique developed originally for finite word automata for tree automata. Subsequently, we improve the antichain technique for both word and tree automata by combining it with the simulation-based inclusion checking techniques, significantly improving efficiency of the antichain method. We then show how the developed reduction and inclusion checking methods improve the method of abstract regular tree model checking, the method that was the original motivation for starting the work on tree automata. Both the reduction and the language inclusion methods are based on relatively simple and general principles that can be further extended for other types of automata and related formalisms. An example is our adaptation of the reduction methods for alternating Büchi automata, which results in an efficient alternating automata size reduction technique.
|
|
Multimedia Data Processing in Heterogeneous Distributed Environment
Kajan, Rudolf ; Ferko,, Andrej (oponent) ; Míkovec, Zdeněk (oponent) ; Herout, Adam (vedoucí práce)
Ubiquitous computing, a paradigm in which the processing of information is linked with each activity or object as encountered, was proposed by Mark Weiser as the next era for interacting with computers. Its goal is to enable people to interact with devices more naturally and casually in ways that suit whatever location or context they find themselves in. Ubiquitous computing focuses on learning by removing the complexity of computing and increases efficiency while using computing for different daily activities. But after more than 15 years since Weiser formulated these goals, several aspects of ubiquitous computing are still not a part of user experience with today’s technology. Seamless integration with environment leading to technological invisibility or user interaction spanning across multiple devices pose still a great challenge. The main goal of our work is to make a step towards making the idea of ubiquitous computing a reality by addressing the question about intuitive information sharing between a personal device and a situated display. We have developed three interaction techniques which support unobtrusive content exchange between touch-enabled personal device and a large display - whether it is shared-private or public. These techniques are based on video streams, augmented reality, and analysis of gaze data. Besides the interaction techniques, we also present a framework for real-time application state acquisition and reconstruction on target platform. We report on user studies focused on the usability of our prototypes and a system performance evaluations. Our experiments were formed around real-life scenarios which are commonly experienced throughout the day. For interactions based on video streams, the results indicate that our techniques outperform the existing solutions: the localization and task migration is done in real time on a midlevel cellphone; the localization is reliable even for different observation angles and for cluttered screen content. Our technique based on gaze analysis goes even further by allowing for modeling of implicit user preferences through gaze data, while being accurate and unobtrusive.
|
|
Intrusion Detection in Network Traffic
Homoliak, Ivan ; Čeleda, Pavel (oponent) ; Ochoa,, Martín (oponent) ; Hanáček, Petr (vedoucí práce)
The thesis deals with anomaly based network intrusion detection which utilize machine learning approaches. First, state-of-the-art datasets intended for evaluation of intrusion detection systems are described as well as the related works employing statistical analysis and machine learning techniques for network intrusion detection. In the next part, original feature set, Advanced Security Network Metrics (ASNM) is presented, which is part of conceptual automated network intrusion detection system, AIPS. Then, tunneling obfuscation techniques as well as non-payload-based ones are proposed to apply as modifications of network attack execution. Experiments reveal that utilized obfuscations are able to avoid attack detection by supervised classifier using ASNM features, and their utilization can strengthen the detection performance of the classifier by including them into the training process of the classifier. The work also presents an alternative view on the non-payload-based obfuscation techniques, and demonstrates how they may be employed as a training data driven approximation of network traffic normalizer.
|
|
Obezita u dětí školního věku z pohledu sestry pracující v ordinaci praktického lékaře
BURSÍKOVÁ, Drahoslava
AAbstrakt Obezita u dětí školního věku z pohledu sestry pracující v ordinaci praktického lékaře Diplomová práce je zaměřena na problematiku ošetřovatelské péče u dětí s nadváhou a obezitou. Tato problematika je v dnešní době velice aktuální a to nejenom v České republice, ale jedná se o celosvětový problém. Naše republika zaujímá jedno z předních míst v obezitě u dětí. Děti trpící nadváhou a obezitou mají nejenom zdravotní problémy plynoucí z komplikací obezity, ale i problémy v oblasti psychiky a sociálních vztahů, zvláště mezi svými vrstevníky. Proto je důležité správné pochopení dané problematiky a nalezení přijatelného řešení do budoucnosti. Teoretická část se zabývá problémem obezity u dětí, specifiky ošetřovatelské péče o tyto děti v rámci ordinace praktického lékaře pro děti a dorost. Zaměřuje se také na potřeby dítěte s normální váhou a potřeby dětí s obezitou. V rámci výzkumného šetření byly stanoveny čtyři cíle. Prvním cílem bylo zmapovat stav obezity u dětí školního a předškolního věku v benešovském okrese. Druhým cílem bylo zmapovat služby (možnosti další pomoci, léčby), které mohou využít rodiče a praktičtí lékaři při léčbě dětí s nadváhou a obezitou v okrese Benešov. Třetím cílem bylo porovnat úspěšnost léčby obezity u dětí, které už podstoupily léčbu obezity pod odborným dohledem s úspěšností snižování nadváhy u dětí, které se snaží o snížení váhy sami. Čtvrtým cílem bylo zmapovat problematiku spolupráce sestry s rodiči a školou v péči o dítě s obezitou. Ve výzkumné části diplomové práce jsme použili metodu kvalitativního výzkumného šetření. Byla zvolena metoda dotazování formou polostrukturovaného rozhovoru. Pro potřeby výzkumu byly vytvořeny tři výzkumné soubory. První výzkumný soubor tvořilo 10 sester, které pracují v ordinaci praktického lékaře pro děti a dorost v okrese Benešov. Druhý výzkumný soubor se skládal z 10 záměrně vybraných osob z řad rodičů dětí s obezitou, které se snaží o redukci váhy svých dětí sami nebo pod odborným dohledem obezitologa. Jednalo se o rodiče dětí předškolního a školního věku. Třetí výzkumný soubor tvořilo 10 praktických lékařů pro děti a dorost, kteří vykonávají svoji praxi na území okresu Benešov. Při zpracování rozhovorů byla použita technika otevřeného kódování metoda papír a tužka. K zmapování služeb v Benešovském okrese a také celém Středočeském kraji byla použita analýza dokumentů. Bylo stanoveno šest výzkumných otázek: 1. Jaké jsou možnosti odborné pomoci obézním dětem? 2. Jsou rodiče ochotni pomoci svým obézním dětem při snižování váhy? 3. Mají rodiče dětí s obezitou také problémy s váhou? 4. Jaké jsou zkušenosti sester v ambulanci praktického lékaře pro děti a dorost v péči o obézní děti? 5. Jak probíhá spolupráce rodičů se sestrou v ambulanci praktického lékaře pro děti a dorost? 6. Jak sestra pracující v ordinaci praktického lékaře pro děti a dorost spolupracuje se školou? Závěry diplomové práce ukazují, že problém dětské obezity je nejenom v benešovském okrese, ale i celosvětově aktuální a má vzestupnou tendenci.
|
|
Úloha sestry v prevenci a léčbě střevních parazitů u dětí
JANDOVÁ, Anna
Mezi nejznámější střevní parazity patří Roup dětský, Škrkavka dětská, Tasemnice a onemocnění nazývané Toxokaróza. Nejčastěji vyskytovaným parazitem je podle zdrojů Roup dětský. Střevní parazité postihují nejčastěji malé děti předškolní věku, někdy i větší. Prvním cílem této bakalářské práce bylo zmapovat informovanost rodičů o prevenci parazitárních onemocnění u dětí. K tomuto cíli byla stanovena hypotéza: Rodiče dětí, které prodělaly parazitární onemocnění, jsou informovanější než rodiče dětí, které parazitární onemocnění neprodělaly. Druhý cíl měl zmapovat specifika ošetřovatelské péče u dětí s parazitárním onemocněním v ordinaci PLDD. K tomuto cíli byla zvolena tato výzkumná otázka: Jaká jsou specifika ošetřovatelské péče u PLDD při parazitárním onemocnění? V metodice byla zvolena empirická část a ta byla zpracována kvalitativně kvantitativním výzkumným šetřením. V kvantitativní části byla použita metoda dotazování a technika nestandardizovaného dotazníku. Výzkumný soubor kvantitativního šetření tvořilo 223 respondentů tedy rodičů, jejichž dítě je ve věku od 0 do 6 let. Dotazníky byly rozdány na sociální síti a další v Mateřské školce v Týně nad Vltavou. Respondenti byli hned v úvodu seznámeni s tématem bakalářské práce. Výsledky kvantitativního šetření byly zpracovány za pomoci datové matice a dále zpracovány do dvaceti přehledných pruhových grafů. K ověření hypotézy jsme použili chí kvadrát test. V kvalitativní části byla použita metoda dotazování, technika hloubkového rozhovoru. Výzkumný soubor tvořilo 5 sester, 3 pracující u PLDD v Týně nad Vltavou a 2 pracující u PLDD v Českých Budějovicích. Při zpracování rozhovorů byla použita metoda otevřeného kódování a analýza rozhovorů byla provedena metodou tužka a papír. Výsledky této bakalářská práce budou publikovány v časopisu Pediatrie pro praxi.
|
|
Zkušenosti zdravotnických pracovníků s akupresurou
ROUBÍČKOVÁ, Radka
Diplomová práce je zaměřena na akupresuru a její ovlivnění bolesti zad u zdravotnických pracovníků. Téma akupresury jsme si vybrali, protože jde o neinvazivní léčebnou metodu, kterou může praktikovat každý člověk i v pohodlí domova a nepotřebuje k tomu žádné pomůcky, pouze základní znalosti a školení, jak akupresuru provádět. Akupresura není fyzicky ani časově náročná, a právě proto ji považujeme za vhodný prostředek jako doplňkovou léčbu bolestí a jiných obtíží ve zdravotnictví. Může posloužit ke zkvalitnění ošetřovatelské péče. Teoretická část se věnuje bolestem celkově a také bolestem u zdravotníků, kteří jsou nejrizikovější skupinou ohroženou bolestí zad nejčastěji v bederní oblasti. U zdravotnických pracovníků bývá bolest zad častou příčinou pracovní neschopnosti. Dále se v teoretické části zabýváme akupresurou, jednou z metod alternativní medicíny. Pro zpracování teoretického základu k dané problematice jsme použili dostupné zahraniční i české literární zdroje. Empirická část diplomové práce je zpracována kvantitativním metodou. Výsledky získané výzkumem byly rozpracovány do přehledných tabulek a kazuistik. Pro diplomovou práci jsme si stanovili dva výzkumné cíle. Prvním cílem bylo zjistit zkušenosti zdravotnických pracovníků s akupresurou. Druhým cílem bylo ověřit vliv technik akupresury na bolesti zad zdravotnických pracovníků. Na základě stanovených cílů práce jsme vytvořili dvě hypotézy. První hypotéza předpokládala, že aplikace akupresurních technik zmírní bolesti zad respondentů. Druhá hypotéza předpokládala, že bude rozdíl v přístupu sester a lékařů k vykonávání akupresury.
|
|
Reflexe díla Františka Bakuleho ve vztahu k dnešní speciálně pedagogické praxi
BALÍKOVÁ, Tereza
František Bakule byl významným českým pedagogem první poloviny 20. století, prvním ředitelem Jedličkova ústavu v Praze, zakladatelem tzv. Bakulova ústavu a jedním z mála českých představitelů alternativního pojetí výchovy a vzdělávání uznávaných v zahraničí. Jeho odkaz však v současné době není naší odbornou veřejností v rámci hlavního vzdělávacího proudu ani speciálních škol dále systematicky rozvíjen a prakticky uplatňován, na rozdíl od řady zahraničních alternativních pedagogických směrů, které jsou zde úspěšně aplikovány. Cílem této bakalářské práce je proto analyzovat dílo Františka Bakuleho prizmatem současného školního edukačního prostředí s důrazem na vzdělávání žáků se zdravotním postižením. První kapitola je věnována nástinu životní cesty Františka Bakuleho, zejména se zaměřením na významné mezníky, které ovlivnily utváření jeho osobnosti, jeho myšlenky, inspiraci a motivaci a které se projevily v jeho pedagogické činnosti a následně v jeho vlastním uceleném konceptu výchovy a vzdělávání. Konkrétně je zde zmíněno jeho rodinné zázemí a dále je prostor věnován zejména jeho učitelským zkušenostem až po působení v Jedličkově ústavu a etapu života spojenou s jeho vlastním ústavem. Druhá část bakalářské práce je již zaměřena výhradně na Bakuleho specifický edukační koncept. Nejprve jsou zde vymezeny jeho principy a následně uvedeny originální učební osnovy a návrh ideálního prostředí třídy. Text dále obsahuje detailní popis výuky několika předmětů, které byly těžištěm Bakuleho konceptu, a to jmenovitě pracovních činností, hudební výchovy a výtvarné výchovy. Původní didaktické postupy jsou analyzovány s využitím současné terminologie. Vzhledem k vymezenému cíli bylo třeba ve třetí kapitole analyzovat současné pojetí vzdělávání ve výše zmíněných, podle Bakuleho stěžejních oblastech. Text je koncipován tak, aby bylo možné následně reflektovat dílo Františka Bakuleho z pohledu dnešní pedagogické, respektive speciálně pedagogické praxe, nalézt styčné body či odlišnosti a odhalit nevyužitý inspirační potenciál. Tomu je pak věnována čtvrtá, závěrečná kapitola. Na základě analýzy a následné reflexe bylo ve výsledku konstatováno, že ačkoli se Bakulem formulované vzdělávací cíle významně neodlišují od současného pojetí zakotveného v příslušných rámcových vzdělávacích programech, k jejich dosažení se v současné době užívá odlišných postupů a metod. A to přestože sám Bakule své postupy, které lze velmi zjednodušeně charakterizovat mottem "neučit žáky o životě a práci, ale životem a prací", s úspěchem ověřil v praxi a že mu v řadě případů daly za pravdu pozdější výsledky psychologických výzkumů, čímž poskytly jeho didaktickému odkazu teoretickou oporu. Z výše uvedeného je zřejmé, že odkaz díla Františka Bakuleho nebyl naší odbornou pedagogickou veřejností dostatečně doceněn a vytěžen. Na druhou stranu je třeba konstatovat, že jeho širšímu uplatnění stojí v cestě roztříštěnost, v níž se nám dochoval.
|
host ::
