|
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.
|
|
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.
|
|
Stability and convergence of numerical computations
Sehnalová, Pavla ; Dalík, Josef (oponent) ; Horová, Ivana (oponent) ; Kunovský, Jiří (vedoucí práce)
The aim of this thesis is to analyze the stability and convergence of fundamental numerical methods for solving ordinary differential equations. These include one-step methods such as the classical Euler method, Runge-Kutta methods and the less well known but fast and accurate Taylor series method. We also consider the generalization to multistep methods such as Adams methods and their implementation as predictor-corrector pairs. Furthermore we consider the generalization to multiderivative methods such as Obreshkov method. There is always a choice in predictor-corrector pairs of the so-called mode of the method and in this thesis both PEC and PECE modes are considered. The main goal and the new contribution of the thesis is the use of a special fourth order method consisting of a two-step predictor followed by an one-step corrector, each using second derivative formulae. The mathematical background of historical developments of Nordsieck representation, the algorithm of choosing a variable stepsize or an error estimation are discussed. The current approach adapts well to the multiderivative situation in variable stepsize formulations. Experiments for linear and non-linear problems and the comparison with classical methods are presented.
|
|
On-line Data Analysis Based on Visual Codebooks
Beran, Vítězslav ; Honec, Jozef (oponent) ; Sojka, Eduard (oponent) ; Zemčík, Pavel (vedoucí práce)
This work introduces the new adaptable method for on-line video searching in real-time based on visual codebook. The new method addresses the high computational efficiency and retrieval performance when used on on-line data. The method originates in procedures utilized by static visual codebook techniques. These standard procedures are modified to be able to adapt to changing data. The procedures, that improve the new method adaptability, are dynamic inverse document frequency, adaptable visual codebook and flowing inverted index. The developed adaptable method was evaluated and the presented results show how the adaptable method outperforms the static approaches when evaluating on the video searching tasks. The new adaptable method is based on introduced flowing window concept that defines the ways of selection of data, both for system adaptation and for processing. Together with the concept, the mathematical background is defined to find the best configuration when applying the concept to some new method. The practical application of the adaptable method is particularly in the video processing systems where significant changes of the data domain, unknown in advance, is expected. The method is applicable in embedded systems monitoring and analyzing the broadcasted TV on-line signals in real-time.
|
|
Security of Contactless Smart Card Protocols
Henzl, Martin ; Rosa, Tomáš (oponent) ; Staudek, Jan (oponent) ; Hanáček, Petr (vedoucí práce)
This thesis analyses contactless smart card protocol threats and presents a method of semi-automated vulnerability finding in such protocols using model checking. Designing and implementing secure applications is difficult even when secure hardware is used. High level application specifications may lead to different implementations. It is important to use the smart card correctly, inappropriate protocol implementation may introduce a vulnerability, even if the protocol is secure by itself. The goal of this thesis is to provide a method that can be used by protocol developers to create a model of arbitrary smart card, with focus on contactless smart cards, to create a model of the protocol, and to use model checking to find attacks in this model. The attack can be then executed and if not successful, the model is refined for another model checker run. The AVANTSSAR platform was used for the formal verification, models are written in the ASLan++ language. Examples are provided to demonstrate usability of the proposed method. This method was used to find a weakness of Mifare DESFire contactless smart card. This thesis also deals with threats not possible to cover by the proposed method, such as relay attacks.
|
|
Intradenní obchody
BOHINSKÝ, Petr
Tato práce je zaměřena na porovnání výnosnosti intradenních a krátkodobých obchodů za použití technické analýzy. Aplikací metody křížení klouzavých průměrů v období 1. ledna 2014 do 1. srpna 2016. Obchodování probíhá na základě nákupních a prodejních signálů generovaného technického indikátoru v investičním programu Alapri a XTB. Obchodovány jsou indexy DAX30, S§P100 a komodity zlato a ropa. Teoretická část práce se věnuje finančnímu trhu, komoditnímu trhu, popisuje intradenního a pozičního obchodníka včetně jejich výhod a nevýhod. Dále se zabývá technickou analýzou a vysvětluje základní investiční výrazy. Praktická část práce se věnuje popisu výsledků vymodelovaných na reálných historických datech. Na základě backtestovaných výsledků lze určit, že metoda křížení klouzavého průměru s hodnotou instrumentu je výhodnější pro krátkodobé obchody, v modelovaném případě na denním grafu než pro intradenní obchody modelovaným na čtyřhodinovém grafu. Dále bylo při modelaci zjištěno, že je výnosnější nakoupit instrumenty a nechat je za daných podmínek zhodnotit finančním trhem. Tedy nakoupit je na začátku investičního období a na konci období prodat bez dalších nákupních a prodejních operací.
|
|
Inovace produktu vybraného podniku cestovního ruchu
JUNGVIRTOVÁ, Kateřina
Tato bakalářská práce se zabývá inovacemi v podniku cestovního ruchu. Cílem práce je zanalyzovat současný produkt firmy a přání a potřeby potencionálních zákazníků. Na základě těchto analýz potom doporučit pro firmu ideální produkt. V této práci spočívá inovace v založení cestovní kanceláře, navrhovaným produktem budou konkrétní zájezdy. V teoretické části se věnuji studiu odborné literatury, konkrétně oblastem produktů, zprostředkovatelů služeb v cestovním ruchu, sportovně rekreačnímu cestovnímu ruchu a vodní turistice. Aplikační část obsahuje charakteristiku společnosti, včetně nabízených služeb. Druhým bodem této části je výzkum. Pro výzkum byla použita metoda přímého dotazování. Dotazování probíhalo přímo v sídle firmy. Respondenty byli lidé, kteří již využili služeb firmy. Pro porovnání očekávaných a získaných výsledků byl u jedné z otázek použit použit chí - kvadrát test. V závěru práce byly sestaveny tři zájezdy, každý upravený speciálně pro konkrétní segment. Návrhová část práce také obsahuje doporučení, jaká opatření musí firma provést, aby její fungování bylo úspěšné.
|
|
Časová náročnost základních ošetřovatelských postupů
SOUMAROVÁ, Iveta
Na odděleních v nemocničním zařízení se denně provádí velké množství ošetřovatelských postupů. Tato bakalářská práce ve své teoretické části představuje dvacet základních postupů. Cílem práce bylo zjistit nejčastější ošetřovatelské postupy a zmapovat jejich časovou náročnost. Pro realizaci cíle byla zvolena kvantitativní metoda výzkumu. Technikou sběru dat bylo měření časové náročnosti deseti jednotlivých ošetřovatelských postupů. Ty byly vybrány proto, že jsou prováděny nejčastěji. Tyto postupy byly pozorovány na interním a chirurgickém oddělení Nemocnice České Budějovice. Na obou odděleních probíhalo prvotní pozorování 3 dny. Z celkového počtu bylo vybráno 10 nejčastějších ošetřovatelských postupů shodných obou oddělení. Zastoupení výkonů bylo hodnoceno chí-kvadrát testem v kontingenční tabulce. Dále se na každém oddělení zvlášť doba provedení každého z deseti nejčastějších výkonů desetkrát změřila, a to od přípravy po úklid pomůcek. Časy byly zprůměrovány a prezentovány spolu se směrodatnými odchylkami. Shoda či rozdíl v časové náročnosti byla statisticky otestována pomoci F testu a T testu, kdy použitá hladina významnosti se rovná 5%. Výzkumný soubor tvořily sestry a pomocný ošetřovatelský personál. Výsledky jsou prezentovány v grafech a tabulkách. Významně se na jednotlivých odděleních lišily tyto postupy: podáváni léků per os, podávání stravy, odběr venózní krve a měření tlaku krve. Zjištěná časová náročnost a četnost jednotlivých výkonů mohou sloužit jako podklad pro zdůvodnění počtu členů personálu.
|
|
Postavení sestry v prevenci civilizačních chorob
PAVLOVÁ, Martina
Současný stav Prevence je komplexní péče o pacienta, kdy se snažíme zabránit vzniku či rozvoji onemocnění, nebo zabránit či zmírnit jeho následky. Preventivní doporučení stanovená lékařem musí mít vědecký základ a jsou součástí všech oborů medicíny. Jejich efektivita je závislá na spolupráci pacientů a zdravotníků. Základní a nejvíce efektivní metodou prevence je podpora zdraví a s ní úzce související zdravotní výchova. Pod pojmem podpora zdraví se skrývá soubor činností a opatření k upevnění a podpoře zdraví. Civilizační choroby jsou skupiny nemocí, které se vyznačují svým spojením s naším životním stylem. Náš organismus je stále více ohrožován nepříznivými vlivy vnějšího prostředí, jako je kvalita ovzduší, pracovní i životní prostředí, nedostatek pohybu, nesprávné stravování, kouření, alkohol. Seznam civilizačních onemocnění se mění spolu se společností a stylem jejího života. V dnešní době se mezi nejčastější řadí kardiovaskulární onemocnění, kam spadá ateroskleróza, hypertenze, infarkt myokardu, cévní mozková příhoda, ischemická choroba srdeční a také obezita. Dále mezi civilizační onemocnění patří diabetes mellitus 2. typu či nádorová onemocnění. Cíle práce Pro tuto práci byly stanoveny dva cíle. Prvním bylo zjistit, jaké je postavení sester v prevenci civilizačních chorob. Druhým cílem bylo zjistit, jaké je postavení sester v prevenci civilizačních chorob z pohledu pacientů. Metodologie Pro výzkumné šetření provedené v této práci byla zvolena kvalitativní metoda s použitím polostrukturovaných rozhovorů. Respondenti byli rozděleni na dvě části, kdy první část tvořilo 8 sester pracujících na interní a neurologické ambulanci českobudějovické nemocnice a setra pracující v soukromé ordinaci obvodního lékaře pro dospělé. Druhou část tvořilo 8 pacientů zmíněných ordinací. Výsledky Podle námi zjištěných odpovědí vidí sestry a pacienti postavení sester jinak. Sestry se v prevenci nemocí spíše vidí vedle lékaře, kdy plní jeho ordinace a pokyny. S pacienty mluví jen, aby mu zdůraznily, co jim sdělil lékař a zopakovali mu nejdůležitější body. Dávají jim k dispozici letáky a brožury, nebo internetové zdroje. Naopak většina pacientů vidí sestru jako důležitější zdroj informací než je lékař. Pacienti mají pocit, že lékař na ně nemá tolik času ani ho nechtějí svými dotazy zdržovat či obtěžovat. Raději se obrátí na sestru, kterou vidí jako svého rádce a někoho komu se mohou svěřit, aniž by ho obtěžovali. Závěr Cílem této bakalářské práce bylo zaměřit se na prevenci, na civilizační choroby a na postavení sestry v prevenci těchto chorob. Prostudovat danou problematiku, nahlédnout na ni očima pacientů a sester díky provedeným rozhovorům a analyzovat tyto informace. Z této analýzy nám vyšla doporučení pro sestry a pacienty.
|
host ::
