This Master’s thesis deals with digital decimation filter design for undersampling and filtering of sigma-delta ADC signal. Filter cascade is designed in Matlab according to given requirements and is then described in VHDL language aiming for minimum area. Implemented filter functionality is compared to Matlab-generated reference filters in created verification environment. Finally the design is synthesized in specified technology and verified on gate level.

This master thesis deals with application of an evolutionary algorithm in the creation of regression tests. In the first section, description of functional verification, verification methodology, regression tests and evolutionary algorithms is provided. In the following section, the evolutionary algorithm, the purpose of which is to achieve reduction of the number of test vectors obtained in the process of functional verification, is proposed. Afterwards, the proposed algorithm is implemented and a set of experiments is evaluated. The results are discussed.

The aim of the master's thesis "Analysis of Selected Payment Protocols" is overview of used payment. The first part is concentrated on data security, the second is dedicated to payment protocols, their characteristics, used technology and security elements. The third part is dedicated to verification and simulation tools. Comparison of particular payment protocols and of particular verification tools is part of this work too. Experimental part of the thesis is focused on formalization and verification of the payment protocol Visa 3-D Secure, of the protocol NetBill and on formalization of two subprotocols of SET.

Tato práce analyzuje hrozby pro protokoly využívající bezkontaktní čipové karty a představuje metodu pro poloautomatické hledání zranitelností v takových protokolech pomocí model checkingu. Návrh a implementace bezpečných aplikací jsou obtížné úkoly, i když je použit bezpečný hardware. Specifikace na vysoké úrovni abstrakce může vést k různým implementacím. Je důležité používat čipovou kartu správně, nevhodná implementace protokolu může přinést zranitelnosti, i když je protokol sám o sobě bezpečný. Cílem této práce je poskytnout metodu, která může být využita vývojáři protokolů k vytvoření modelu libovolné čipové karty, se zaměřením na bezkontaktní čipové karty, k vytvoření modelu protokolu a k použití model checkingu pro nalezení útoků v tomto modelu. Útok může být následně proveden a pokud není úspěšný, model je upraven pro další běh model checkingu. Pro formální verifikaci byla použita platforma AVANTSSAR, modely jsou psány v jazyce ASLan++. Jsou poskytnuty příklady pro demonstraci použitelnosti navrhované metody. Tato metoda byla použita k nalezení slabiny bezkontaktní čipové karty Mifare DESFire. Tato práce se dále zabývá hrozbami, které není možné pokrýt navrhovanou metodou, jako jsou útoky relay.

This diploma thesis deals with the issue of information transfer between the Department of Electrical Equipment Design and the Software Development Department of the control system of this machine. The diploma thesis focuses mainly on the elimination of the influence of the human factor while increasing the efficiency of this information transfer. System analysis examines the issues and investigates the reliability of information transfer. On the basis of the requirements resulting from the analysis, preventive measures and modifications of procedures in both departments have been proposed. Simultaneously, its own software applications have been developed to considerably simplify and accelerate the process, while meeting the requirements to eliminate problematic phenomena caused particularly by human factors. The resulting solution is verified according to the designated verification process and reassessed by own "SampleVUT" test project. Validation evaluates the effectiveness of the proposed solution.

Modern network traffic processing became a challenging task as there are increasing demands on network security devices. Packet-level processing is not sufficient for advanced network traffic analysis and it is necessary to design processing over entire network flows. Stateful processing in software does not offer enough performance for high-speed networks over 10 Gbps and therefore acceleration in hardware should be utilized. Currently there exists no universal platform for stateful processing in hardware and this task has to be implemented individually. Utilization of such platform significantly speed-up development of stateful network applications. This master thesis analyzes all aspects of stateful network processing platform design. Component based architecture increases platform flexibility and ability to optimize for chosen network applications.

This thesis is aimed to specify and implement multi-purpose framework able to deal with graphical real-time system specification. This tool allows to use arbitrary verification approach to resulting system model check. Description of basic formal specification methods based on mathematic logic is done. Some well-known hierarchical graphical specifications for real-time systems are depictured. Author proposed suitable cases for functionality examination of resulting framework.

Ph.D. thesis is focused on the design of the method for simulation of energy demands of machine tool in operation at the stage of its development. Proposed method is developer on the basis of literature search in science and in industry. The method itself is composed of five related steps, that must be realised in the proper order in order to create a relevant energy profile of a machine tool. The output from the method are simulated data providing a course of comsumed energy and required power which are time dependent. Output data are obtained on the basis of the drive system simulation of machine tool through G-code, that is interpreted for simulation by the compiler into the matrix. It contains data necessary for controlling of machine tool, such as the required end points of the tool and required feed rates, to which is assigned a time value. G-code is partially time parametrized. It is then followed by full time parametrization through a of mathematical model of drive mechanisms and due the synergy of software for drive mechanisms control (Matlab Simulink) and software for physical simulation (MSC Adams) is processed into output data. As an input parameter figures also coefficient used as multiplier of the normal force of driving mechanisms, which is a function of feed rate. This loss function is obtained experimantally. In the context of Ph.D. thesis were conducted two experiments, used to verify the developed method. For each experiment is proceeded according to estabilished method and it is included a comparsion of simulation and measured data for various operating modes. The proposed method, described in the Ph.D. thesis, allows designers to summarize the energy demand of the proposed machine before its production. When correctly interpreted, the results of the method can serve as a basis for improving the energy profile and thereby increasing the energy efficiency of the machine tool.

The aim of this thesis is to provide an overview of some of the commonly used methods in the area of authorship attribution (stylometry). The text begins with a recap of history from the end of the 19th century to present time and the required terminology from the field of text mining is presented and explained. What follows is a list of selected methods from the field of multidimensional statistics (principal components analysis, cluster analysis) and machine learning (Support Vector Machines, Naive Bayes) and their application as pertains to stylometrical problems, including several methods created specifically for use in this field (bootstrap consensus tree, contrast analysis). Finally these same methods are applied to a practical problem of authorship verification based on a corpus bulit from the works of four internet writers.

Ph.D. thesis is focused on the design of the method for simulation of energy demands of machine tool in operation at the stage of its development. Proposed method is developer on the basis of literature search in science and in industry. The method itself is composed of five related steps, that must be realised in the proper order in order to create a relevant energy profile of a machine tool. The output from the method are simulated data providing a course of comsumed energy and required power which are time dependent. Output data are obtained on the basis of the drive system simulation of machine tool through G-code, that is interpreted for simulation by the compiler into the matrix. It contains data necessary for controlling of machine tool, such as the required end points of the tool and required feed rates, to which is assigned a time value. G-code is partially time parametrized. It is then followed by full time parametrization through a of mathematical model of drive mechanisms and due the synergy of software for drive mechanisms control (Matlab Simulink) and software for physical simulation (MSC Adams) is processed into output data. As an input parameter figures also coefficient used as multiplier of the normal force of driving mechanisms, which is a function of feed rate. This loss function is obtained experimantally. In the context of Ph.D. thesis were conducted two experiments, used to verify the developed method. For each experiment is proceeded according to estabilished method and it is included a comparsion of simulation and measured data for various operating modes. The proposed method, described in the Ph.D. thesis, allows designers to summarize the energy demand of the proposed machine before its production. When correctly interpreted, the results of the method can serve as a basis for improving the energy profile and thereby increasing the energy efficiency of the machine tool.