Diploma thesis deals with design of verification environment for analyzing systems with digital filters. Verification environment is written in SystemVerilog language and it is generated by program, which is also providing generation of input data for system of filters. Matlab environment is used for gaining the reference data. The simulation of the designed involvement with digital filters is performed by program ModelSim. The most watched parameter is functional coverage which indicates how big part of the HDL description has been tested.

Textual use-cases have been traditionally used at the design stage of the software development process to describe software functionality from the user's perspective. Because use-cases typically rely on natural language, they cannot be directly subject to formal verification. Another important artefact is the domain model, a high-level overview of the most important concepts in the problem space. A domain model is usually not constructed en bloc, yet it undergoes refinement starting from the first prototype elicited from text. This thesis covers two closely related topics - formal verification of use-cases and elicitation of a domain model from text. The former is a method (called FOAM) that features simple user-definable annotations inserted into a use-case to make it suitable for verification. A model-checking tool is employed to verify temporal invariants associated with the annotations while still keeping the use-cases understandable for non-experts. The latter is a method (titled Prediction Framework) that features an in-depth linguistic analysis of text and a sequence of statistical classifiers (log-linear Maximum Entropy models) to predict the domain model.

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.

In the development process of digital circuits, it is often not possible to avoid introducing errors into systems that are being developed. Early detection of such errors saves money and time. This project deals with automation of feedback in functional verification of various data processing components. The goal of automatic feedback is not only to shorten the time needed to verify the functionality of a system, but mainly to improve verification coverage of corner cases and thus increase the confidence in the verified system. General functional and formal verification principles and practices are discussed, coverage metrics are presented, limitations of both techniques are mentioned and room for improvement of current status is identified. Design of feedback verification environment using a genetic algorithm is described in detial. The verification results are summarized and evaluated.

In the present work we study opportunities of mapping the XML data into relational systems. In the first part we describe basic terminology used in this work and subsequently also basic techniques for mapping XML data into the relational database. In the next part we engaged in theoretical methods like MXM and ShreX, which were proposed on premises of a university or by a research group. In the third part we describe mapping methods, that are used in some commercial systems like Oracle, DB2 and MS SQL. In the whole second half of this work we propose a new mapping method (XRM), which bring in several new features, while the origin positive features are kept. At the end we analyze the prototype implementation of the proposed mapping method.

Title: Presenting results of software model checker via debugging interface Author: Tomáš Kohan Department: Department of Software Engineering Supervisor of the master thesis: RNDr. Ondřej Šerý, Ph.D., Department of Distributed and Dependable Systems Abstract: This thesis is devoted to design and implementation of the new debugging interface of the Java PathFinder application. As a suitable inte- face container was selected the Eclipse development environment. The created interface should visualize results of JPF and details of paused JVM state, es- pecially a list of variables and their values. Two subprojects were created, i.e. debug4jpf and JPFDeb.core. The first one is responsible for controlling and communication with the JPF instance. The latter one is an Eclipse plugin and provides user interface which is similar to the interface of standard Java debugger. These two components communicate with each other by using the ad-hoc communication protocol created for this purpose. Keywords: Java, verification, model checker, JPF, debugging interface

The aim of this thesis is empirical verification of the fundamental theory of exchange rate determination in the case of the currency pair EUR/USD. The theoretical part is devoted to the issue of exchange rate theory, with emphasis on the importance of the currency pair EUR/USD, and major characteristics of the fundamental theory of exchange rate determination. Attention is also paid to methods of analysis of time series, which will be used in the analytical part. The analytical part is devoted to an empirical verification of the underlying theories. On the basis of these theories are developed econometric models, which are then tested using the methods of linear regression and cointegration. The results of the models and their relevance are discussed in conclusion.

Title: Presenting results of software model checker via debugging interface Author: Tomáš Kohan Department: Department of Software Engineering Supervisor of the master thesis: RNDr. Ondřej Šerý, Ph.D., Department of Distributed and Dependable Systems Abstract: This thesis is devoted to design and implementation of the new de- bugging interface to the Java PathFinder application. As a suitable interface container was selected the Eclipse development environment. The created inter- face visualizes results of JPF and details of paused JVM state, especially a list of variables and their values. Two subprojects were created, i.e. debug4jpf and JPFDeb.core. The first one is responsible for controlling and communication with the JPF instance. The latter one is an Eclipse plugin and provides user interface which is similar to the interface of standard Java debugger. These two components communicate with each other by using the ad-hoc communication protocol created for this purpose. Keywords: Java, verification, model checker, JPF, debugging interface

The thesis deals with numerical simulation of temperature field with internal heat sources and experimental verification of this model in an environment where the high temperatures are applied (during thermal modification of wood). The work was further extended by analysis of coupled heat and monture transfer in the wood. Designed mathematical models are solved numerically using software COMSOL Multiphysics based on the finite element analysis (FEM). The chemical reactions occur due to decomposition of woodconstituents (cellulose, hemicelluloses and lignin) are taken into account in present study. These reactions are usually not solid in known models. The results of numerical simulations of temperature field, including pyrolysis model, are compared with experimental measurements for verification of the proposed model. Contribution of this thesis is the possible application of the proposed model for the design and optimization of thermal modification Schedule with respekt to wood species and sample dimensions.

This thesis analyses comparison and verification of three global numeric weather models, GFS, ECMWF, NEMS. The research subjects are make comparison of their 48-hour forecast with, for this thesis created, index correspondence of models and evaluate predictability of weather. Next, introduce basic verification methods and their application to forecast verification, from previously mentioned models, against surface observations with resolution 2 ř x 2 ř lat/lon between 1. 6. 2017-28. 2. 2018. Results show, that the worst predictability is at areas with continental glaciers, extensive world mountain ranges and at ITCZ area. The best predictability is observed in subtropical anticyclones over the oceans. Verification of temperature we find out significant smoothing of diurnal cycle in all three models. Biases of relative humidity are strongly negative corelated with temperature bias, skill score for relative humidity is worse than for temperature. Performance of mean sea level pressure is the best for all verification metrics from all analysed quantities. Wind speed is for most world overestimated. Results of 3-hour precipitation depends on treshold. Models overestimate frequency of low intensity precipitation, opposite results are observed for high intensity precipitation, break occur at interval...