|
|
Transducers in Automata Library Mata
Chocholatý, David ; Lengál, Ondřej (referee) ; Holík, Lukáš (advisor)
Implementujeme konečné převodníky do nové rychlé a jednoduché automatové knihovny Mata. Konečné převodníky jsou konečné stavové stoje modelující regulární relace. Naše hlavní použití pro konečné převodníky je kódovaní operací nahrazení (nahrazení slova nebo regulárního vzoru řetězcem). Nový SMT nástroj pro řešení formulí s omezeními nad řetězci Z3-Noodler používá knihovnu Mata jako základ pro jeho rozhodovací proceduru. Noodler potřebuje konečné převodníky k analýze programů manipulujících s řetězci s operacemi nahrazení. Analýzou zmíněných programů používaných ve webových aplikacích se zabrání útokům jako cross-site scripting (XSS) nebo vložení kódu. Hlavní odlišující vlastnosti knihovny Mata zahrnují jednoduchost (jednoduchá k užívání, úpravě a rozšíření) a efektivitu (pracuje rychle). Reprezentaci a algoritmy pro konečné převodníky jsme navrhli s ohledem na tyto vlastnosti knihovny. K reprezentaci konečných převodníků a jejich algoritmů znovupoužijeme a rozšíříme existující datové struktury a algoritmy pro konečné automaty v knihovně Mata. Reprezentace pro konečné převodníky slouží jako společná reprezentace pro konečné převodníky a budoucí reprezentaci automatů využívajících multi-terminálních binárních rozhodovacích diagramů pro práci s velkými abecedami. Navíc rozšíříme návrh o algoritmy pro konstrukci konečných převodníků modelujících operace nahrazení definovaných v SMT-LIB. Nakonec experimentálně vyhodnotíme efektivitu konečných převodníků v knihovně Mata na nové sadě příkladů s operacemi nahrazení z běhů nástroje Z3-Noodler a z řešení problémů nalezení vzoru.
|
|
|
Složení snímku prstu s viditelným krevním řečištěm.
Pekárek, Jakub ; Semerád, Lukáš (referee) ; Rydlo, Štěpán (advisor)
This thesis describes a method for creating a composite image with a visible bloodstream. The bloodstream is detected by the Maximum Curvature algorithm. After that it was experimented with detecting and matching keypoints via algorithms SIFT and ORB. However, the resulting matches from these algoritms were not good enough, therefore the keypoints have to be manually assigned. From these keypoints, an estimated tranformation matrix was created. This matrix was then used for connecting two images. A cycle of assigning keypoints and connecting images is repeated even for newly created images. The final composite image with a visible bloodstream is created after connecting last two images. This composite image can be further used for verification or identification people.
|
|
|
Automata in Verification
Šmahlíková, Barbora ; Holík, Lukáš (referee) ; Lengál, Ondřej (advisor)
Regulární model checking je technika pro verifikaci nekonečněstavových systémů založená na automatech. Konfigurace systému jsou dány konečným automatem a přechody mezi nimi konečným převodníkem. Algoritmus pro verifikaci libovolných vlastností parametrických systémů specifikovaných v temporální logice LTL(MSO) již existuje. V této práci představíme rozšíření tohoto algoritmu, které umožňuje verifikaci hypervlastností parametrických systémů, tedy vlastností, ve kterých lze explicitně kvantifikovat nad několika cestami v systému. Specifikujeme podmínky, které musí platit pro dvojici tzv. advice bitů (složené z konečného automatu a konečného převodníku), která slouží jako svěděk toho, že je daná vlastnost v systému splněna. Algoritmus představený v této práci je implementovaný v nástroji ParaHyper - jediném existujícím nástroji pro verifikaci hypervlastností parametrických systémů. Tento nástroj využívá SAT solveru pro generování automatů a převodníků. Pokud je nalezen takový pár, který vyhovuje podmínkám pro advice bity, vlastnost je v systému splněna. Bylo provedeno experimentální vyhodnocení představeného algoritmu a bylo zjištěno, že ParaHyper je schopen generovat advice bity pro formule s abecedou až o 4 symbolech, pokud mají automat i převodník nejvýše 2 stavy. Pokud jsou však automat i převodník zadány uživatelem, ParaHyper umí efektivně zkontrolovat, zda vyhovují podmínkám i v případě větších abeced a většího počtu stavů.
|
|
|
FFT implementation in FPGA and ASIC
Dvořák, Vojtěch ; Bohrn, Marek (referee) ; Fujcik, Lukáš (advisor)
The aim of this thesis is to design the implementation of fast Fourier transform algorithm, which can be used in FPGA or ASIC circuits. Implementation will be done in Matlab and then this form of implementation will be used as a reference model for implementation of fast Fourier transform algorithm in VHDL. To verify the correctness ofdesign verification enviroment will be created and verification process wil be done. Program that will generate source code for various parameters of the module performing a fast Fourier transform will be created in the last part of this thesis.
|
|
|
Test Planning Tool Extension for Distributed Systems
Mészáros, Filip ; Ráb, Jaroslav (referee) ; Ščuglík, František (advisor)
This bachelor thesis is about automatical software testing using the testing scheduler. It describes creation of the extension for the existing testing scheduler, so it will be possible to split effectively a group of tests to segments, that will be executed independently on each other. Tests are splitted according to the common characteristics of the enviroment, that need to be prepared for each test, and according to the dependencies between the tests. Furthermore, it describes what optimizations are used for splitting of the tests to subsets. Each subset of the tests runs on a standalone testing system, so the time needed for succesful completion of testing with the given set of tests is reduced. Created tool is succesfully used during everyday testing of the several products in the Acision company, to which was this tool made.
|
|
|
Functional Verification Framework for Multi Buses Following the UVM Standard
Beneš, Tomáš ; Šišmiš, Lukáš (referee) ; Kekely, Lukáš (advisor)
This thesis focus on the design and subsequent implementation of a multi-bus verification environment using the principles of the Universal Verification Methodology (UVM). It also focus on the implementation of the verification of three FPGA components using multi-bus as input and output interfaces. The implementation of the environment and all verifications is written in SystemVerilog language using a library that implement the basic constructs for UVM. The achieved results of the work are functional and easily reusable when creating further verifications using multi-bus. The proposed environments can be used as a structure for creating other verification environments for other buses.
|
|
|
Biometry based on retinal videosequences
Oweis, Kamil ; Odstrčilík, Jan (referee) ; Kolář, Radim (advisor)
The biometric methods are the most advanced methods for recognition and verification of person identity. These methods are quite fast, safe and applicable in different situations. In this thesis is used a set of retinal scans taken with a video-ophtalmoscope. These pictures are further modified for next processing, first of all by convertion into black-andwhite binary image, in some cases was after that used a binary matrix for description of image. Afterwards was suggested comparison method of images from the database with reference image of the retina: method of overlap and shift. It was tested a set of blackand-white and then also grey images. All method calculations was realized in program Matlab of which outcome was determination of the most congruent image with reference image and evaluation of overall program accuracy.
|
|
|
Handwriting and Signature Verification
Beránek, Jan ; Řezníček, Ivo (referee) ; Španěl, Michal (advisor)
This paper concerns methods of verification of person's signature and handwriting. Some of commonly used techniques are resumed and described with related literature being referred. Next aim of this work is design and implementation of a simple handwriting verification application. Application is based on edge detection and comparison of a set of structural and statistical features. As a support classification tool a SVM classifier of the LIBSVM software is employed. The Application is written in C language using OpenCV graphics library. Testing and training set was extracted from samples found in the IAM Handwriting Database. Application was created and tested in the Windows XP operating system.
|
|
|
Data Structure Visualization for Verification Tools
Holubec, Michael ; Lengál, Ondřej (referee) ; Peringer, Petr (advisor)
The aim of my bachelor thesis is an object-oriented design and implementation of a library which will provide a unified interface to a verification tool Predator and other tools for making a vizualization of data structures primarily for debuging purposes. This work analyses some qualities of the verification tool Predator, Forester and CPAchecker. The library offers not only a graphic but also a text-based output in DOT language. The result has been tested by connecting to the verification tool Predator.
|
|
|
Test Driven Development for FPGA Designs
Halász, Dávid ; Strnadel, Josef (referee) ; Šimek, Václav (advisor)
Tato bakalářská práce popisuje, jak může být princip TDD uplatněn u hardware, převážně pro vývoj FPGA. Je popsána důležitá teorie pro pochopení kontextu. Na referenčním návrhu jsou představeny některé dostupné a užitečné verifikační nástroje. Jeden z těchto nástrojů byl vybrán a pomocí TDD byl vytvořen a úspěšně otestován návrh komunikačního modulu SPI.
|
guest ::
