The diploma thesis deals with experimental determination of hydrodynamic load on the overflowed bridge deck model. In the first part of the thesis the author describes the analysis of the problem together with the basic physical laws and principles that are used or assumed in the measurement itself. In the second part the author describes the measurements in the laboratory of the Faculty of Civil Engineering and its gradual processing. At the end of the work are described the results of measurement, their comparison with numerical modeling, other authors and their possible use in practice.

The aim of the diploma thesis is application of the topic Control of HVAC equipments. The thesis is divided into three part – A, B, C. The first theoretical part deals with controlling/regulation in general, it focuses on controlling/regulation of HVAC equipments and it describes ways of air volume flow measurement, which relates to the third experimental part. The second part is focused on design of HVAC system in inpatient ward and fit-out for employees. In the third part was realized verification of air flow volume controller in two chosen buildings, whence in one there weren´t fulfilled manufacturer´s requirements and in the second one they were fulfilled. In conclusion there were compared measured values.

Mnoho aplikací přijímá, odesílá a zpracovává data v textové podobě. Správné a bezpečné zpracování těchto dat je typicky zajištěno tzv. ošetřením řetězců (string sanitization). Pomocí metod formální verifikace je možné analyzovat takovéto operace s řetězci a prověřit, zda jsou správně navržené či implementované.  Naším cílem je vytvořit obecný nástroj pro analýzu systémů jejichž konfigurace lze kódovat pomocí slov z vhodné abecedy, a také jeho specializaci pro analýzu programů pracujících s řetězci. Nejprve jsou popsaný konečné automaty a převodníky a poté různé třídy a podtřídy symbolických převodníků, zejména pak jejich omezení. Na základě těchto informací je pak pro použití v analýze programů navržen nový typ symbolických převodníků. Dále je popsán regulární model checking, speciálně pak jeho variantu založenou na abstrakci automatů, tzv. ARMC, u kterého je známo že dokáže velmi úspěšně překonat problém stavové exploze u automatů a umožňuje nám tzv. dosáhnout pevného bodu v analýze. Poté je navržena vlastní analýza programů psaných v imperativním paradigmatu, a to zejména programů manipulujících s řetězci, založená na principech ARMC. Následuje popis vlastní implementace nástroje s důrazem na jeho praktické vlastnosti. Rovněž jsou popsaný důležité části knihovny AutomataDotNet, na které nástroj staví. Práci je uzavřena diskuzí experimentů s nástrojem provedených na příkladech z knihovny LibStranger.

This work deals with the text-dependent speaker recognition in systems, where just a few training samples exist. For the purpose of this recognition, the voice imprint based on different features (e.g. MFCC, PLP, ACW etc.) is proposed. At the beginning, there is described the way, how the speech signal is produced. Some speech characteristics important for speaker recognition are also mentioned. The next part of work deals with the speech signal analysis. There is mentioned the preprocessing and also the feature extraction methods. The following part describes the process of speaker recognition and mentions the evaluation of the used methods: speaker identification and verification. Last theoretically based part of work deals with the classifiers which are suitable for the text-dependent recognition. The classifiers based on fractional distances, dynamic time warping, dispersion matching and vector quantization are mentioned. This work continues by design and realization of system, which evaluates all described classifiers for voice imprint based on different features.

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.

This document is trying to introduce the reader with issues of identifying the face connected with miscellaneous scanning technologies and enviroments. Inside this document there are mentioned some possibilities of creation unique print of a face so that there would be denied unwanted effects of enviroment and the identification of persons would be possible.

Tato práce se zaměřuje na konečné automaty nad konečnými slovy a konečnými stromy, a použití těchto automatů při formální verifikaci nekonečně stavových systémů. Práce se nejdříve věnuje rozšíření existujícího přístupu pro verifikaci programů které manipulují s haldou (konkrétně programů s dynamickými datovými strukturami), jenž je založen na stromových automatech. V práci je navrženo několik rozšíření tohoto přístupu, jako například jeho plná automatizace či jeho rozšíření o podporu uspořádaných dat. V práci jsou popsány nové rozhodovací procedury pro dvě logiky, které jsou často používány ve formální verifikaci: pro separační logiku a pro slabou monadickou druhořádovou logiku s následníkem. Obě tyto rozhodovací procedury jsou založeny na převodu jejich problému do automatové domény a následné manipulaci v této cílové doméně. Posledním přínosem této práce je vývoj nových algoritmů k efektivní manipulaci se stromovými automaty, s důrazem na testování inkluze jazyků těchto automatů a manipulaci s automaty s velkými abecedami, a implementace těchto algoritmů v knihovně pro obecné použití. Tyto vyvinuté algoritmy jsou použity jako klíčová technologie, která umožňuje použití výše uvedených technik v praxi.

This project deals with given safeguard possibilities, both mechanical and electronic. A row house with garden was chosen for being secured. Subsequently, were elaborated two`s proposals of securing and guarding of this object. First, was based on camera`s system and second on common system ESS. Later on they were evaluated and the most considerable benefits were emphasized. A system based on control panel with connected detectors was selected upon specification. Subsequently was created a model of the chosen system, at which the required behaviour was simulated and verified. An outline of an implementation was created in the C language.