|
Relational Verification of Programs with Integer Data
Konečný, Filip ; Bouajjani, Ahmed (referee) ; Jančar, Petr (referee) ; Vojnar, Tomáš (advisor)
Tato práce představuje nové metody pro verifikaci programů pracujících s neomezenými celočíslenými proměnnými, konkrétně metody pro analýzu dosažitelnosti a~konečnosti. Většina těchto metod je založena na akceleračních technikách, které počítají tranzitivní uzávěry cyklů programu. V práci je nejprve představen algoritmus pro akceleraci několika tříd celočíselných relací. Tento algoritmus je až o čtyři řády rychlejší než existující techniky. Z teoretického hlediska práce dokazuje, že uvažované třídy relací jsou periodické a~poskytuje tudíž jednotné řešení prolému akcelerace. Práce dále představuje semi-algoritmus pro analýzu dosažitelnosti celočíselných programů, který sleduje relace mezi proměnnými programu a~aplikuje akcelerační techniky za účelem modulárního výpočtu souhrnů procedur. Dále je v práci navržen alternativní algoritmus pro analýzu dosažitelnosti, který integruje predikátovou abstrakci s accelerací s cílem zvýšit pravděpodobnost konvergence výpočtu. Provedené experimenty ukazují, že oba algoritmy lze úspěšně aplikovat k verifikaci programů, na kterých předchozí metody selhávaly. Práce se rovněž zabývá problémem konečnosti běhu programů a~dokazuje, že tento problém je rozhodnutelný pro několik tříd celočíselných relací. Pro některé z těchto tříd relací je v práci navržen algoritmus, který v polynomiálním čase vypočítá množinu všech konfigurací programu, z nichž existuje nekonečný běh. Tento algoritmus je integrován do metody, která analyzuje konečnost běhů celočíselných programů. Efektivnost této metody je demonstrována na několika netriviálních celočíselných programech.
|
|
Stability and convergence of numerical computations
Sehnalová, Pavla ; Dalík, Josef (referee) ; Horová, Ivana (referee) ; Kunovský, Jiří (advisor)
Tato disertační práce se zabývá analýzou stability a konvergence klasických numerických metod pro řešení obyčejných diferenciálních rovnic. Jsou představeny klasické jednokrokové metody, jako je Eulerova metoda, Runge-Kuttovy metody a nepříliš známá, ale rychlá a přesná metoda Taylorovy řady. V práci uvažujeme zobecnění jednokrokových metod do vícekrokových metod, jako jsou Adamsovy metody, a jejich implementaci ve dvojicích prediktor-korektor. Dále uvádíme generalizaci do vícekrokových metod vyšších derivací, jako jsou např. Obreshkovovy metody. Dvojice prediktor-korektor jsou často implementovány v kombinacích modů, v práci uvažujeme tzv. módy PEC a PECE. Hlavním cílem a přínosem této práce je nová metoda čtvrtého řádu, která se skládá z dvoukrokového prediktoru a jednokrokového korektoru, jejichž formule využívají druhých derivací. V práci je diskutována Nordsieckova reprezentace, algoritmus pro výběr proměnlivého integračního kroku nebo odhad lokálních a globálních chyb. Navržený přístup je vhodně upraven pro použití proměnlivého integračního kroku s přístupe vyšších derivací. Uvádíme srovnání s klasickými metodami a provedené experimenty pro lineární a nelineární problémy.
|
|
Extensions to Probabilistic Linear Discriminant Analysis for Speaker Recognition
Plchot, Oldřich ; Fousek, Petr (referee) ; McCree,, Alan (referee) ; Burget, Lukáš (advisor)
Tato práce se zabývá pravděpodobnostními modely pro automatické rozpoznávání řečníka. Podrobně analyzuje zejména pravděpodobnostní lineární diskriminační analýzu (PLDA), která modeluje nízkodimenzionální reprezentace promluv ve formě \acronym{i--vektorů}. Práce navrhuje dvě rozšíření v současnosti požívaného PLDA modelu. Nově navržený PLDA model s plným posteriorním rozložením modeluje neurčitost při generování i--vektorů. Práce také navrhuje nový diskriminativní přístup k trénování systému pro verifikaci řečníka, který je založený na PLDA. Pokud srovnáváme původní PLDA s modelem rozšířeným o modelování neurčitosti i--vektorů, výsledky dosažené s rozšířeným modelem dosahují až 20% relativního zlepšení při testech s krátkými nahrávkami. Pro delší testovací segmenty (více než jedna minuta) je zisk v přesnosti menší, nicméně přesnost nového modelu není nikdy menší než přesnost výchozího systému. Trénovací data jsou ale obvykle dostupná ve formě dostatečně dlouhých segmentů, proto v těchto případech použití nového modelu neposkytuje žádné výhody při trénování. Při trénování může být použit původní PLDA model a jeho rozšířená verze může být využita pro získání skóre v případě, kdy se bude provádět testování na krátkých segmentech řeči. Diskriminativní model je založen na klasifikaci dvojic i--vektorů do dvou tříd představujících oprávněný a neoprávněný soud (target a non-target trial). Funkcionální forma pro získání skóre pro každý pár je odvozena z PLDA a trénování je založeno na logistické regresi, která minimalizuje vzájemnou entropii mezi správným označením všech soudů a pravděpodobnostním označením soudů, které navrhuje systém. Výsledky dosažené s diskriminativně trénovaným klasifikátorem jsou podobné výsledkům generativního PLDA, ale diskriminativní systém prokazuje schopnost produkovat lépe kalibrované skóre. Tato schopnost vede k lepší skutečné přesnosti na neviděné evaluační sadě, což je důležitá vlastnost pro reálné použití.
|
|
Query-by-Example Spoken Term Detection
Fapšo, Michal ; Matoušek, Jindřich (referee) ; Metze, Florian (referee) ; Černocký, Jan (advisor)
Tato práce se zabývá vyhledáváním výrazů v řeči pomocí mluvených příkladů (QbE STD). Výrazy jsou zadávány v mluvené podobě a jsou vyhledány v množině řečových nahrávek, výstupem vyhledávání je seznam detekcí s jejich skóre a časováním. V práci popisujeme, analyzujeme a srovnáváme tři různé přístupy ke QbE STD v jazykově závislých a jazykově nezávislých podmínkách, s jedním a pěti příklady na dotaz. Pro naše experimenty jsme použili česká, maďarská, anglická a arabská (levantská) data, a pro každý z těchto jazyků jsme natrénovali 3-stavový fonémový rozpoznávač. To nám dalo 16 možných kombinací jazyka pro vyhodnocení a jazyka na kterém byl natrénovaný rozpoznávač. Čtyři kombinace byly tedy závislé na jazyce (language-dependent) a 12 bylo jazykově nezávislých (language-independent). Všechny QbE systémy byly vyhodnoceny na stejných datech a stejných fonémových posteriorních příznacích, pomocí metrik: nesdružené Figure-of-Merit (non pooled FOM) a námi navrhnuté nesdružené Figure-of-Merit se simulací normalizace přes promluvy (utterrance-normalized non-pooled Figure-of-Merit). Ty nám poskytly relevantní údaje pro porovnání těchto QbE přístupů a pro získání lepšího vhledu do jejich chování. QbE přístupy použité v této práci jsou: sekvenční statistické modelování (GMM/HMM), srovnávání vzorů v příznacích (DTW) a srovnávání grafů hypotéz (WFST). Abychom porovnali výsledky QbE přístupů s běžnými STD systémy vyhledávajícími textové výrazy, vyhodnotili jsme jazykově závislé konfigurace také s akustickým detektorem klíčových slov (AKWS) a systémem pro vyhledávání fonémových řetězců v grafech hypotéz (WFSTlat). Jádrem této práce je vývoj, analýza a zlepšení systému WFST QbE STD, který po zlepšení dosahuje podobných výsledků jako DTW systém v jazykově závislých podmínkách.
|
|
Intrusion Detection in Network Traffic
Homoliak, Ivan ; Čeleda, Pavel (referee) ; Ochoa,, Martín (referee) ; Hanáček, Petr (advisor)
Tato práce se zabývá problematikou anomální detekce síťových útoků s využitím technik strojového učení. Nejdříve jsou prezentovány state-of-the-art datové kolekce určené pro ověření funkčnosti systémů detekce útoků a také práce, které používají statistickou analýzu a techniky strojového učení pro nalezení síťových útoků. V další části práce je prezentován návrh vlastní kolekce metrik nazývaných Advanced Security Network Metrics (ASNM), který je součástí konceptuálního automatického systému pro detekci průniků (AIPS). Dále jsou navrženy a diskutovány dva různé přístupy k obfuskaci - tunelování a modifikace síťových charakteristik - sloužících pro úpravu provádění útoků. Experimenty ukazují, že použité obfuskace jsou schopny předejít odhalení útoků pomocí klasifikátoru využívajícího metriky ASNM. Na druhé straně zahrnutí těchto obfuskací do trénovacího procesu klasifikátoru může zlepšit jeho detekční schopnosti. Práce také prezentuje alternativní pohled na obfuskační techniky modifikující síťové charakteristiky a demonstruje jejich použití jako aproximaci síťového normalizéru založenou na vhodných trénovacích datech.
|
|
The Pump with a Diffuser with Stochastic Blades (Runner and Diffuser)
Dobšáková, Lenka ; Melichar, Jan (referee) ; Veselý, Jindřich (referee) ; Haluza, Miloslav (advisor)
This doctoral thesis studies the non-uniform blade cascade for centrifugal pumps. Influence of non-uniform blade cascade is investigated on the impeller and diffuser. A non-uniform blading impeller of pumps in this doctoral thesis was examined in terms of influence on efficiency characteristic. The idea of using non-uniform blading is to obtain a flat efficiency characteristic. Then the centrifugal pump could be used on larger scale of power with achieving a sufficiently high efficiency. The work is based on experimental measurements and numerical simulations of non-uniform hydraulic pump components. Non-uniform impeller and the diffuser were newly designed for this research. A new measuring track of small submersible pumps was needed to design and build for measurements. Different pump combinations with conventional hydraulics on one working point and hydraulics with non-uniform were measured. All measurements were evaluated and characteristics of efficiency, head and power were obtained for each measured combination. Some of pump combinations (which were measured in experiment) were numerically simulated by program Ansys Fluent. Data needed to evaluate the characteristic of efficiency and specific energy were collected from each numerical simulation. A theoretical consideration concerns the influence of non-uniform blade cascade applied on diffuser. The suggestion how to decrease hydraulic losses in canals was done. The theoretical consideration how to make a flat efficiency characteristic was made.
|
|
Vývoj metodologické a technologické platformy pro neinvazivní odhad fenolických látek v listech a bobulích
ŠEBELA, David
Plant optical signals can serve as important source of information about biochemical and physiological processes in plants. These signals are influenced by compounds synthesized by plants during primary or secondary metabolism and thus, can also serve as their qualitative and quantitative indicators. Light reaching plant surface (leaf or fruit) can undergo three main pathways- it can be (i) reflected, (ii) absorbed or it can (iii) transmit through plant material. The probability of these three processes depends on particular wavelength of incident irradiation and on the morphological characteristics of plant tissues themselves. As such, plant contains various spectrum of photosynthetic pigments and fluorescent compounds which can either reflect, absorb or pass incident irradiation through at specific wavelengths. Biophysical techniques working with these optical properties of plant pigments and/or other compounds have become universal and common tool in basic and applied research. To quote some example, chlorophyll fluorescence imaging, UV induced fluorescence or spectroscopic techniques are on the top of interest thanks to its non-invasive nature, allowing maintain the integrity of measured cells or the whole plant constituents. The main aim of this thesis is to provide a comprehensive study on the possibility of non-invasive monitoring of phenolic compounds in the leaves and fruits.
|
|
Injuries of children at home
POCHYLÁ, Petra
The theoretical part of this thesis is oriented at an actual issue of accidents involving children in home environment, their prevention and a correct provision of first aid by a non-professional at these types of selected accidents. The practical part of this thesis was led by a qualitative form of research, a method of a semicontrolled interview. The interview given was led by chosen caring people, who gave first aid to children with a home environment injury. The whole process of the interview was recorded at a digital record book and then rewritten to a text form, with the approval of the respondents. The respondents were chosen on the basis of a survey. The final information from the interviews were analyzed and subsequently summarized into results. Six respondents were registered into the research part. Six basic questions were given to the respondents. The questions were chosen to find out information about an injured child, an injury character, a procedure of caring person while giving first aid, or other professional care and permanent effects. While preparing the research part, I was expecting that most of the respondents would manage to give first aid, however, according to the results, half of the parents didn't know how to deal with giving first aid. Non- professional first aid, provided at the right time and done correctly, is one of the basic and essential steps to reverse the injured person back into the normal quality of life. This is why, all people should be able to give first aid without special equipment and tools. The aim of my thesis was to monitor the process of the caring person while giving first aid for selected accidents involving children in home environment. I gave myself one fundamental research question: What was the process of the caring person while giving first aid for accidents involving children in home environment? At the final evaluation and comparison of my results, I achieved the results, in most examined facts, which are presented in other different studies dealing with similar issues- children's injuries and giving first aid for accidents involving children.
|
|
THE DRAMATICAL SCRIPT AS A NECESSARY BASIS FOR SPACIAL REALIZATOIN
Tretiag, Štěpán ; KORČÁK, Jakub (advisor) ; HRBEK, Daniel (referee)
Using the concrete examples of my practical bachelor work my intent is to retrospectively describe and reflect on our scenic realization of the play Missing by south-African author Reza de Wet. The essence of a modern dramatic direction is to perceive the script of a play as a model which becomes a basis for its interpretation and the subsequent staging of the play. It is the process from the initial interpretation to final scenic realization I wish to focus on in my work.In the first part I will be dealing with creation of a physical space, that being stage design. I will try to capture what lead us to its final shape and how the basis for that can be found in the script of the play as well as the potential capability of the physical space to become a dramatic space. Its ability to create a platform for the actors to proceed from and how can it provoke them into acting, in particular. In the second part I will be dealing with the dramatic space, ergo the spacial expression of relationships and themes. I will proceed again retrospectively, focusing on how we managed to achieve the stage image which is functioning as a materialized metaphor. I will focus mostly on non-verbal actions, but with regard to the fact, that dramatical script is the basis for our realization of the play.
|
|
Healthy aging in the context of nursing care
RADOVÁ, Ludmila
Healthy Ageing Programme is a concept which should have a significant influence on every resident in the countries where population median age has been quickly increasing. This topic of healthy ageing is the key issue of the given Master´s Diploma Thesis. At the present, our country is involved not only in several smaller-scale regional programmes focused on lives of seniors but also in the events of European importance. If we want to provide our seniors with a quality life in all aspects, it is necessary to encourage promoting Healthy Ageing Programme. The wide scope of activity is thus open, especially for nurses. The first objective develops the approach of seniors in the selected health-care facilities to healthy ageing. The second objective introduces the approach of a client before retirement age to the healthy ageing principles. Finally, the third objective specifies the role of general practice nurses in their support of clients before retirement age in their healthy ageing. Research questions included the following issues: the approach of a client at the age before retirement to the healthy ageing principles and the role of a general practice nurse and her support of the abovementioned clients. The given research also develops one hypothesis regarding the fact that personal objectives will change depending on barriers.Both qualitative and quantitative research was used in the given Diploma Thesis. An in-depth interview was conducted during the survey. Additional information was obtained on the basis of an opinion poll. Two research groups were used for the interview: the first one consisted of 11 respondents from the general practitioner´s outpation departments, the second research group consisted of 6 nurses working for the aforementioned departments. The total number of 150 respondents from the designated health-care facilities was selected for the survey during which they were answering the research questions. As a result, a large number of useful information was obtained. The clients' approach can be divided into several groups: leisure activities, education, workload, prevention and medical examinations, regimen, community nursing care, healthy ageing. The key roles of a nurse should take into consideration the following aspects: healthy ageing from the nurse´s point of view, prevention and geriatric nurse at the outpatient department, community nursing care, health support of the patients provided by a nurse. Information obtained from the interviews were interconnected and often corresponded with each other. Research questions are also followed by the given results. A nurse has a significant role in the area of education, provision of necessary information to the clients, promotion of prevention programmes informing the clients about the solution to their problems. The motivation of clients before retirement age is also crucial because it is at this age when people can influence their life, its length and quality. The survey also observes the general perception of people of an old age and changes in their point of view with age. The information collected from this survey may be also used in different studies in order to improve both quality of nursing care and motivation of the clients before their retirement.
|
guest ::
