|
|
Transducers in Automata Library Mata
Chocholatý, David ; Lengál, Ondřej (oponent) ; Holík, Lukáš (vedoucí práce)
We implement finite transducers in a new fast and simple automata library Mata. Finite transducers are finite state machines modelling rational relations. Our primary use case for finite transducers is encoding replace operations (replacing a word or a regular pattern with a string literal). A recent automata-based SMT string solver Z3-Noodler uses Mata as a backbone of its decision procedure. Z3-Noodler needs finite transducers to analyse string manipulating programs with replace operations. The analysis of said programs used in web applications prevents software attacks such as cross-site scripting (XSS) or code injection. The distinctive features of Mata include simplicity (simple to use, modify and extend) and efficiency (fast to run). We design the representation and algorithms for finite transducers to fit the simplicity and efficiency requirements. We inherit and extend the existing data structures and algorithms for finite automata in Mata to represent the finite transducers and their operations. The representation for finite transducers serves as a common data structure and interface for the finite transducers and future representation of automata using multi-terminal binary decision diagrams to handle large alphabets. We further extend the design with algorithms to construct finite transducers modelling replace operations defined in SMT-LIB. Finally, we run an experimental evaluation of performance of finite transducers in Mata on a new benchmark with replace operations from runs of Z3-Noodler and from solving problems in pattern matching.
|
|
|
Složení snímku prstu s viditelným krevním řečištěm.
Pekárek, Jakub ; Semerád, Lukáš (oponent) ; Rydlo, Štěpán (vedoucí práce)
Práce popisuje zpracování snímku prstu pro vytvoření kompozitního snímku s viditelným krevním řečištěm. Krevní řečiště je detekováno algoritmem Maximum Curvature. Následně bylo experimentováno s hledáním a spojování klíčových bodů pomocí algoritmů SIFT a ORB. Protože však algoritmy nepřinášely požadované výsledky, musí být klíčové body vyznačovány manuálně. Z nich je vytvořen odhad matice transformace. Pomocí odhadu matice transformace je spojena dvojice snímků. Tento cyklus přiřazení klíčových bodů a spojení snímků probíhá i pro nově vytvořené snímky. Po spojení posledních dvou snímků je výsledkem kompozitní snímek s viditelným krevním řečištěm. Tento kompozitní snímek může být dále využit pro verifikaci nebo identifikaci osob.
|
|
|
Automata in Verification
Šmahlíková, Barbora ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
Regular model checking is an automata-based technique used for verification of infinite-state systems. The configurations of a system are encoded as a finite automaton and transitions between these configurations as a finite transducer. A technique for verifying arbitrary properties of parameterized systems specified in a temporal logic LTL(MSO) has already been introduced. We present an extension of this algorithm allowing verification of hyperproperties of parameterized systems where an explicit quantification over multiple execution traces is allowed. We specify conditions that need to hold for a pair of advice bits (a finite automaton and a finite transducer) that serves as a witness of the fact that the property holds in the system. The technique presented in this work is implemented in our tool ParaHyper - the only existing tool for the verification of hyperproperties of parameterized systems. The tool uses a SAT solver to generate automata and transducers. If a pair satisfying the conditions for advice bits is found, the property holds in the system. We performed an experimental evaluation of our approach and found that ParaHyper is able to generate advice bits for formulae with an alphabet up to 4 symbols if both the automaton and the transducer have at most 2 states. When a candidate pair is given by the user, ParaHyper can, however, efficiently check if it satisfies the conditions for advice bits even for larger alphabets and greater number of states.
|
|
|
Implementace výpočtu FFT v obvodech FPGA a ASIC
Dvořák, Vojtěch ; Bohrn, Marek (oponent) ; Fujcik, Lukáš (vedoucí práce)
Cílem diplomové práce je navrhnout implementaci algoritmu rychlé Fourierovi transformace, kterou lze použít v obvodech FPGA nebo ASIC. Implementace bude modelována v prostředí Matlab a následně bude použit tento návrh jako referenční model pro popis implementace algoritmu rychlé Fourierovy transformace v jazyce VHDL. Pro ověření správnosti návrhu bude vytvořeno verifikační prostředí a provedena verifikace. V poslední části práce bude navržen program, který bude generovat zdrojové kódy pro různé parametry modulu provádějícího rychlou Fourierovu transformaci.
|
|
|
Rozšíření plánovače testů pro distribuované systémy
Mészáros, Filip ; Ráb, Jaroslav (oponent) ; Ščuglík, František (vedoucí práce)
Tato bakalářská práce se zabývá automatickým testováním softwaru s použitím plánovače testů. Popisuje tvorbu rozšíření existujícího plánovače testů tak, aby bylo možné efektivně rozdělit skupinu testů na části, které se budou vykonávat nezávisle na sobě. Jednotlivé testy jsou rozdělovány na základě společných vlastností prostředí, které je pro tyto testy nutno připravit, a na základě závislostí mezi testy. Práce dále popisuje, jaké optimalizace jsou použity pro rozdělování testů do podmnožin. Každá podmnožina testů je spouštěná na samostatném testovacím systému a tím je snížen čas potřebný pro otestování testovaného softvéru danou sadou testů. Vytvořený nástroj se úspěšně používá při každodenním testování několika produktů ve firmě Acision, pro kterou byl tento nástroj vytvářen.
|
|
|
Prostředí pro funkční verifikaci multi-sběrnic podle UVM standardu
Beneš, Tomáš ; Šišmiš, Lukáš (oponent) ; Kekely, Lukáš (vedoucí práce)
Práce se zabývá návrhem a následnou implementací prostředí pro verifikace multi-sběrnic s využitím principů univerzální verifikační metodologie (UVM). Dále se zabývá implementací verifikací tří FPGA konkrétních komponent využívající multi-sběrnice jako vstupní a výstupní rozhraní. Implementace prostředí i všech verifikací je napsaná v jazyce SystemVerilog s využitím knihovny implementující základní konstrukce pro UVM. Dosažené výsledky práce jsou funkční a jednoduše znovupoužitelné při tvorbě dalších verifikací využívající multi-sběrnic. Navržené prostředí se dají využít jako struktura pro tvorbu dalších verifikačních prostředí pro jiné sběrnice.
|
|
|
Statistická přejímka
Vyškovský, Jaroslav ; Fiala, Alois (oponent) ; Pernikář, Jiří (vedoucí práce)
Tato práce řeší statistickou přejímkou kontrolu velkých objemů produktů dovážených do České republiky. Práce jako taková je konstruována tak, aby bylo možno danou metodiku užít i u jiných aplikací a produktů než na jaké bylo navrženo konkrétní řešení. Vypracování této práce bylo provedeno ve spolupráci s firmou, zabývající se segmentem spojovacích prvků pro dřevozpracující průmysl. Využity byly dostupné standardy, jak pro určení potřebných charakteristik jakosti produktů, tak pro tvorbu samotné metodiky. Závěrem této práce je technické a ekonomické zhodnocení navržené metodiky, provedené na modelovém zastupujícím produktu.
|
|
|
Biometrie s využitím videosekvencí sítnice
Oweis, Kamil ; Odstrčilík, Jan (oponent) ; Kolář, Radim (vedoucí práce)
Biometrické metody jsou nejmodernější způsob pro rozpoznání a ověření totožnosti osob. Jsou poměrně rychlé, bezpečné a použitelné v různých situacích. V této práci je použita sada snímků oční sítnice získaných použitím video oftalmoskopu. Snímky jsou dále upraveny pro další zpracování, nejprve převedením na černobílý binární obraz, v některých případech pak byla použita binární matice pro popis daného snímku. Poté byla navržena metoda srovnání snímků databáze s referenčním snímkem oční sítnice nazvaná metoda překrytí a posunu. Byla testována sada černobílých a poté i šedých snímků. Všechny výpočty metody byly realizovány v programu Matlab, jehož výsledkem bylo určení nejvíce shodného snímku se snímkem referenčním a vyhodnocení celkové přesnosti programu.
|
|
|
Verifikace rukopisu a podpisu
Beránek, Jan ; Řezníček, Ivo (oponent) ; Španěl, Michal (vedoucí práce)
Tato práce se zabývá metodami verifikace ručně psaného podpisu a rukopisu. Shrnuje a popisuje některé užívané techniky a odkazuje na příslušnou literaturu. Dalším tématem práce je návrh a implementace jednoduché aplikace pro verifikaci rukopisu. Aplikace je založena na hranové detekci a porovnání vybraných strukturálních a statistických příznaků. Jako podpůrný nástroj pro rozhodování je použit SVM klasifikátor z balíku LIBSVM. Aplikace je napsána v jazyce C a využívá grafickou knihovnu OpenCV. Testovací i trénovací sada byla vytvořena ze vzorků rukopisu z internetové databáze IAM Handwriting Database. Aplikace je vytvořena a testována v prostředí operačního systému Windows XP.
|
|
|
Koncept rychlonabíjecí stanice pro elektromobily s akumulací
Miškovský, Ján ; Morávek, Jan (oponent) ; Mastný, Petr (vedoucí práce)
Predmetom tejto práce je vytvorenie konceptu rýchlonabíjacej stanice s akumuláciou a využitím obnoviteľných zdrojov. V úvodnej časti diplomovej práce je popísaná normou stanovená špecifikácia nabíjania elektromobilu za použitia technológie striedavého alebo jednosmerného prúdu a vytvorený prehľad možností použitia nabíjacích konektorov. Prvá časť taktiež obsahuje prehľad technológie obnoviteľných zdrojov energie s využitím akumulácie pre nabíjaciu stanicu. V druhej časti práce na základe teoretických podkladov je vytvorený matematický model nabíjacej stanice v prostredí Matlab/Simulink. Funkčnosť modelu stanice je verifikovaná s fyzikálnym laboratórnym modelom. Pre overenie možnosti pripojenia stanice k distribučnej sieti je vytvorená simulácia úbytkov napätí v prostredí Matlab/Simulink. Následne v práci sú nasimulované štyri 24 hodinové scenáre. Podľa predpokladov simulácie je navrhnutá technológia stanice a prepojenie jednotlivých komponentov. Následne je vypracovaná energetická a finančná analýza projektu nabíjacej stanice do roku 2030.
|
host ::
RSS.