|
New Methods for Increasing Efficiency and Speed of Functional Verification
Zachariášová, Marcela ; Dohnal, Jan (referee) ; Steininger, Andreas (referee) ; Kotásek, Zdeněk (advisor)
Při vývoji současných číslicových systémů, např. vestavěných systému a počítačového hardware, je nutné hledat postupy, jak zvýšit jejich spolehlivost. Jednou z možností je zvyšování efektivity a rychlosti verifikačních procesů, které se provádějí v raných fázích návrhu. V této dizertační práci se pozornost věnuje verifikačnímu přístupu s názvem funkční verifikace. Je identifikováno několik výzev a problému týkajících se efektivity a rychlosti funkční verifikace a ty jsou následně řešeny v cílech dizertační práce. První cíl se zaměřuje na redukci simulačního času v průběhu verifikace komplexních systémů. Důvodem je, že simulace inherentně paralelního hardwarového systému trvá velmi dlouho v porovnání s během v skutečném hardware. Je proto navrhnuta optimalizační technika, která umisťuje verifikovaný systém do FPGA akcelerátoru, zatím co část verifikačního prostředí stále běží v simulaci. Tímto přemístěním je možné výrazně zredukovat simulační režii. Druhý cíl se zabývá ručně připravovanými verifikačními prostředími, která představují výrazné omezení ve verifikační produktivitě. Tato režie však není nutná, protože většina verifikačních prostředí má velice podobnou strukturu, jelikož využívají komponenty standardních verifikačních metodik. Tyto komponenty se jen upravují s ohledem na verifikovaný systém. Proto druhá optimalizační technika analyzuje popis systému na vyšší úrovni abstrakce a automatizuje tvorbu verifikačních prostředí tím, že je automaticky generuje z tohoto vysoko-úrovňového popisu. Třetí cíl zkoumá, jak je možné docílit úplnost verifikace pomocí inteligentní automatizace. Úplnost verifikace se typicky měří pomocí různých metrik pokrytí a verifikace je ukončena, když je dosažena právě vysoká úroveň pokrytí. Proto je navržena třetí optimalizační technika, která řídí generování vstupů pro verifikovaný systém tak, aby tyto vstupy aktivovali současně co nejvíc bodů pokrytí a aby byla rychlost konvergence k maximálnímu pokrytí co nejvyšší. Jako hlavní optimalizační prostředek se používá genetický algoritmus, který je přizpůsoben pro funkční verifikaci a jeho parametry jsou vyladěny pro tuto doménu. Běží na pozadí verifikačního procesu, analyzuje dosažené pokrytí a na základě toho dynamicky upravuje omezující podmínky pro generátor vstupů. Tyto podmínky jsou reprezentovány pravděpodobnostmi, které určují výběr vhodných hodnot ze vstupní domény. Čtvrtý cíl diskutuje, zda je možné znovu použít vstupy z funkční verifikace pro účely regresního testování a optimalizovat je tak, aby byla rychlost testování co nejvyšší. Ve funkční verifikaci je totiž běžné, že vstupy jsou značně redundantní, jelikož jsou produkovány generátorem. Pro regresní testy ale tato redundance není potřebná a proto může být eliminována. Zároveň je ale nutné dbát na to, aby úroveň pokrytí dosáhnutá optimalizovanou sadou byla stejná, jako u té původní. Čtvrtá optimalizační technika toto reflektuje a opět používá genetický algoritmus jako optimalizační prostředek. Tentokrát ale není integrován do procesu verifikace, ale je použit až po její ukončení. Velmi rychle odstraňuje redundanci z původní sady vstupů a výsledná doba simulace je tak značně optimalizována.
|
|
Simulace a protiřetězce pro efektivní práci s konečnými automaty
Holík, Lukáš ; Černá, Ivana (referee) ; Jančar, Petr (referee) ; Vojnar, Tomáš (advisor)
Cílem této práce je vývoj technik umožňujících praktické využití nedeterministických konečných automatů, zejména nedeterministických stromových automatů. Jde zvláště o techniky pro redukci velikosti a testování jazykové inkluze, jež hrají zásadní roli v mnoha oblastech aplikace konečných automatů. V oblasti redukce velikosti vycházíme z dobře známých metod pro slovní automaty které jsou založeny na relacích simulace. Navrhli jsme efektivní algoritmy pro výpočet stromových variant simulačních relací a identifikovali jsme nový typ relace založený na kombinaci takzvaných horních a dolních simulací nad stromovými automaty. Tyto kombinované relace jsou zvláště vhodné pro redukci velikosti automatů slučováním stavů. Navržený princip kombinace relací simulace je relevantní i pro slovní automaty. Náš přínos v oblasti testování jazykové inkluze je dvojí. Nejprve jsme zobecnili na stromové automaty takzvané protiřetězcové algoritmy, které byly původně navrženy pro slovními automaty. Dále se nám podařilo použitím simulačních relací výrazně zefektivnit protiřetězcové algoritmy pro testování jazykové inkluze jak pro slovní, tak pro stromové automaty. Relevanci našich technik pro praxi jsme demonstrovali jejich nasazením v rámci regulárního stromového model checkingu, což je verifikační metoda založená na stromových automatech. Použití našich algoritmů zde vedlo k výraznému zrychlení a zvětšení škálovatelnosti celé metody. Základní myšlenky našich algoritmů pro redukci velikosti automatů a testování jazykové inkluze jsou aplikovatelné i na jiné typy automatů. Příkladem jsou naše redukční techniky pro alternující Büchiho automaty prezentované v poslední části práce.
|
|
On-line Data Analysis Based on Visual Codebooks
Beran, Vítězslav ; Honec, Jozef (referee) ; Sojka, Eduard (referee) ; Zemčík, Pavel (advisor)
Práce představuje novou adaptabilní metodu pro on-line vyhledávání videa v reálném čase pomocí vizuálních slovníků. Nová metoda se zaměřuje na nízkou výpočetní náročnost a přesnost vyhledání při on-line použití. Metoda vychází z technik využitých u statických vizuálních slovníků. Tyto běžné techniky jsou upraveny tak, aby byly schopné se adaptovat na proměnlivá data. Postupy, které toto u nové metody řeší, jsou - dynamická inverzní frekvence dokumentů, adaptabilní vizuální slovník a proměnlivý invertovaný index. Navržený postup byl vyhodnocen na úloze vyhledávání videa a prezentované výsledky ukazují, jaké vlastnosti má adaptabilní metoda ve srovnání se statickým přístupem. Nová adaptabilní metoda je založena na konceptu plovoucího okna, který definuje, jakým způsobem se vybírají data pro adaptaci a ke zpracování. Společně s konceptem je definován i matematický aparát, který umožňuje vyhodnotit, jak koncept nejlépe využít pro různé metody zpracování videa. Praktické využití adaptabilní metody je konkrétně u systémů pro zpracování videa, kde se očekává změna v charakteru vizuálních dat nebo tam, kde není předem známo, jakého charakteru vizuální data budou.
|
|
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í.
|
|
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.
|
|
Biochemical methods as tool for study of reproductive proteins
Postlerová, Pavla ; Zigo, Michal ; Pohlová, Alžběta ; Jonáková, Věra
Study of molecular mechanisms in reproduction is essential for the understanding of this outstanding process. Our lab studies proteins secreted by reproductive organs and sperm using various biochemical methods for a long time. We have expertise in protein extraction from spermatic cells using different approaches, and by kits for proteins from the sperm surface and distinct subcellular compartments. The proteins of reproductive organ fluids are separated by chromatographic methods, such as size exclusion chromatography, high-performance liquid chromatography with reverse phase (RP-HPLC) and affinity chromatography on matrices with various ligands. Proteins are subjected to SDS- or 2D-electrophoresis for their characterization and comparison of various extraction methods, different mammalian species, and sperm in different functional development. Electrophoretically separated proteins may be transferred onto nitrocellulose membrane (Western blot) for antibody detection or binding studies with lectin-labelled ligands (lectins, polysaccharides, zona pellucida glycoproteins). We use immunoprecipitation method with specific antibody for protein determination followed by the MALDI identification. Proteins are localized by immunofluorescent techniques on/in spermatic cells and tissue sections of reproductive organs. Isolation of proteins from reproductive tissues and fluids, and the antibody detection is crucial for the studying of reproductive protein origin.
|
|
Dynamics of mouse sperm capacitation and acrosome reaction
Dvořáková-Hortová, Kateřina ; Frolíková, Michaela ; Děd, Lukáš ; Šebková, Nataša
Capacitation followed by the acrosome reaction (AR), is a very complex event of molecular changes, including acrosome matrix rearrangement and actin polymerization, which mammalian sperm must undergo in the female reproductive tract in order to obtain the ability to penetrate and fertilize the egg. CD46 and β1-integrin belong to specific proteins, which are predicted to interact during molecular reorganization of capacitating sperm. The IZUMO1 as the primary fusion protein of the mammalian sperm is also involved in this dynamic network. We investigated the relationship between the Izumo, CD46 and β1 integrin relocation in the sperm head during the capacitation and AR in vitro. We have already successfully monitored by immunofluorescent labelling the dynamics of proteins CD46 and β1-integrin. The changes in the localization of these proteins associated with the AR and their mutual co-localization was observed. The original β1-integrin location in the freshly released epididymal sperm is in the acrosome and it relocates during the AR further through the sperm head compartments into the equatorial segment and over the whole sperm head. Its density over the equatorial segment is decreasing with the extended time of the AR. Also its presence in the perforatorium of the mouse sperm head is very prominent. The pattern for protein CD46 is extremely similar if not identical in both aspects such as compartment localization and time progress during capacitation and AR in vitro. The molecular interaction of CD46 and β1-integrin was investigated using the Proximity Ligation Assay and Super resolution microscopy STED. The data were statistically analysed. The newly obtained results from CD46 and β1-integrin relocation are in correlation with IZUMO1 dynamics and giving a substantial knowledge on the studied protein network rearrangement during capacitation and AR in mouse spermatozoa.
|
|
International Digital Library of Manuscripts
Knoll, Adolf,
The Manuscriptorium Digital Library is Europe’s largest digital library of manuscripts providing access to data from more than 120 institutions across Europe incl. ca. 55 most important Czech collections. In March 2015, it contained 43,372 fully digitized documents and more than 337,000 bibliographic records. The documents are not only of European origin (Western, Slavonic, Hebrew, Armenian ...), but there are also data representing Arabic, Persian, Ottoman, Indian and other manuscript traditions. The digital library was launched in 2003 by the National Library of the Czech Republic, in partnership with the Czech AiP Beroun Company. In comparison and in contrast with other aggregation services, it provides seamless access to full digital documents on the fly, reusing thus repositories of partner digital libraries. Users do not need to travel or to navigate from one physical place or digital library to another one to access needed documents. Manuscriptorium provides uniform interface to any data from any digital library that signed the partnership agreement. The internal metadata solution is based on the robust TEI P5 approach and suits both library and researchers’ requirements for description and structuring. It aggregates not only fully digitized documents, but also the partially digitized ones and bibliographic records. It contains manuscripts as well as old printed books, historical maps, and historical posters. The documents are mostly represented by digital images and in certain extent also by full texts, TEI-structured and unstructured. The Manuscriptorium larger environment provides also online support to TEI authoring and online metadata validation and upload. ...
|
|
The Use of the Addictive Drugs by the Seniors
KOPAČKOVÁ, Dominika
The bachelor thesis deals with using addictive substances by senior citizens. The age cathegoty 60+ should not be omitted when speaking of using addictive substances. Even senior citizens are users of some addictive substances, especially drugs. The thesis is divided into two parts, theoretical and explorative one. There are four chapters in the theoretical part (Old age and ageing, Substance addiction, Addictive substances and their classification, Usage of addictive substances in the old age) and summarizes the knowledge from recent literature about this topic. First, the old age and ageing are described. This chapter deals with ageing and old age of the human. This work describes the right mental hygiene, too. Multi-factorial manifestation of the old age (biological, psychological and social) is mentioned as well. In the second chapter there are described the factors that increase probability of the addiction origin. These factors can be genetic, biological, and psychological. There are mentioned some system models of the formation, development and maintenance of addiction, dependence and definition of the signs that addiction manifests. The third chapter divides addictive substances between legal and illegal. There are their effects, impacts on the human organism decribed. The group of legal addictive substances are included tobacco, alcohol, drugs and certain foods. Illegal substances represented here by cannabis, hallucinogens, stimulants, opiates. The last fourth chapter focuses directly on the addictive behaviour of the senior citizens. Seniors are also users of substances with addictive potential. At first alcoholism is mapped, other chapters devote addiction to nicotine, drugs and narcotics. The main goal of the thesis is to determine whether seniors use an addictive substance. A partial goal of is to find out the extent and cause of using addictive substances by the senior population. To find out these goals there were used the principles of quantitive research. To collect the data there were used questionnaires, created all by the author. The questionnaires were created with open and closed questiones and used in the printed form. The research has been conducted in Sušice and its close surroundings in February 2015. Respondents were the people with the least age limit of 70 years. These were 40 people living in their households or home for elderly. The results show that also amongst senior citizens can be found those ones who use the addictive substances. Current problem are by the doctor prescribed drugs. Today´s senior citizen uses drugs regularly, very often also combination of more drugs. Seniors often use medication to relieve the pain because the pain occurs more frequently. They use drugs to help them sleep better, too. The next group of addictive substances, which this chapter deals with, are drugs with a shoothing effect. There are smokers between the senior citizens who bare this bad habit from their midlife. Some research shows that cannabis helps people with Parkinson's and Alzheimer´s disease. Seniors do not use cannabis for these purposes because it is not legal. Alcohol is drunk by older people on occassion, on the other hand there are also people who drink such an amount that is not considered as not-risky. Seniors do not drink so much on one occasion, compared to the young generation. In the thesis this problem is described more detailed. Results of the research can be used by lay public to understand issues of addictive substances better. This thesis can be source of information for students of healt-social fields of study and it can improve the awareness about reasons of using addictive substances amongs senior citizens.
|
|
The reflection of František Bakule's work in a relation to a current special educational practice
BALÍKOVÁ, Tereza
František Bakule was a significant Czech teacher during the first half of the 20th century. He was known as the first director of the "Jedlicka Institute in Prague" as well as the founder of so-called "Bakule´s Institute" as well as one of the few representatives of the "Czech alternative approach towards education" which is very well recognized all around the world. His legacy and teachings, however, are currently not being developed on the systematic level and neither they are being put into practise by Czech professional mainstream educational community. We also need to mention that is not used by even the stream of special education, in contrast to many foreign alternative pedagogical trends, which are gaining popularity and are generally applied with success. The aim of this thesis is therefore to analyse the work of Frantisek Bakule through the prism of contemporary school educational environment with emphasis on the education of students with disabilities. The first chapter is devoted to outlining the life journey of Frantisek Bakule, particularly focusing on the major milestones that influenced the formation of his personality, his ideas, inspiration and motivation which was reflected in his teachings and then in his very own coherent concept of education. To be specific, we are introduced to his family background and a significant part is then devoted to description of Frantisek´s experience as a teacher, including stages of operating in Jedlicka´s Institute and in his own "Bakule´s institute". The second part is then focused solely on Bakule´s specific educational concept. First, the core principles of the concept are defined. Later parts then talk about Bakule´s original curriculum and a his proposal of an ideal classroom environment. The text also contains a detailed description of how Bakule approached several subjects, which were at the core of his teaching concept, namely "Work activities", "Music education" and "Arts". Original teaching practices are analysed by using current teaching methodology and terminology. Due to the identified aim and goals of the thesis, the third chapter analyses the current concept of education of the above, according to Bakule´s core areas and principles. The text is designed specifically to be subsequently reflecting the work of Frantisek Bakule from the perspective of today's teaching methods, namely the methods of special education. The idea is to define common points and possible differences and uncover hidden inspirational potential, which is then the main content of the fourth and final chapter. Based on the analysis and all its subsequent reflections, the final chapter tells us that although Bakule´s educational goals don´t differ too significantly from the current concept embedded in the relevant framework of educational programs, to achieve such goals we are currently using very different techniques and methods in comparison to Bakule´s ways. Even though Bakule himself tested and verified all of his concepts in practice, which can be very simply described as "do not teach students about life and work, but through life and work", and these concepts also have been proven correct by various subsequent results of psychological researches, the current system still doesn´t draw from them too much. From all the above it is quite obvious that the legacy of life´s work of Frantisek Bakule is currently not utilized nor it is being appreciated by our professional pedagogical community. On the other hand, we need to note that it may also be due to the level of fragmentation in which his concept and materials were preserved to the present days.
|
guest ::
