|
|
Hierarchical Modeling of Planning Problems
Dvořák, Tomáš ; Barták, Roman (advisor) ; Plátek, Martin (referee)
Automated planning is a task to find a sequence of actions leading from an initial state to a desired goal state. There is a lot of formal models for planning problems modeling. The class of hierarchical formal models is one of them. In this thesis we will propose a hierarchical model, called GramPlan, based on attribute grammars. We will present some methods to reduce classical STRIPS formalism to GramPlan and we will prove the correctness of this reduction. Also we will present reduction of the FlowOpt workflow model to GramPlan and we will prove it's correctness. We will desing a couple of verification methods for attribute grammars and we will show these methods are equivalent. Powered by TCPDF (www.tcpdf.org)
|
|
|
From textual specification to formal verification
Šimko, Viliam ; Hnětynka, Petr (advisor) ; Gruhn, Volker (referee) ; Steinberger, Josef (referee)
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.
|
|
|
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.
|
|
|
The usage of Impact FEM workbench for task solution in the field of solid mechanics
Ferenc, Filip ; Kubík, Petr (referee) ; Vosynek, Petr (advisor)
This bachelor thesis is focused on calculating the main tasks in the field of solid mechanic with usage Impact FEM. At the beginning, there is some basic information about a numerical calcu-lation focusing on the Finite element method. The second part deals with Impact FEM pro-gramme description and model preparation. The main part of this thesis are examples of the tasks which I evaluated by Impact FEM. Results of those calculations were compared to the results obtained by analytic calculations and programme Ansys Workbench. Based on those verification calculations, I consider the Impact FEM programme is not able to calculate the main tasks of solid mechanic at this moment but it may be useful as a learning tool.
|
|
|
FPGA Implementation of RMAP Initiator and Target
Walletzký, Ondřej ; Fujcik, Lukáš (referee) ; Dvořák, Vojtěch (advisor)
The thesis deals with design and implementation of controllers for the RMAP protocol, which is used by SpaceWire network endpoints to access memory contents of another endpoint. The theoretical research introduces concepts of the SpaceWire network, then describes the RMAP protocol and the AMBA AHB bus interface in detail. The practical part of this thesis then uses this information to design and implement controllers for the RMAP protocol. It first defines an architecture of these controllers, then describes design of individual blocks based on this architecture. As a next step, the thesis describes methods used to verify designed controllers and to test these controllers in an FPGA chip. Finally, an analysis of maximum frequency and usage of FPGA resources is done based on estimates provided by the synthesis tool.
|
|
|
Quality control of molecular biology methods in transplantation medicine
Kotrbatý, Jiří ; Kolesár, Libor (advisor) ; Schierová, Michaela (referee)
This work is focused on the description of quality control of molecular-biological methods used in transplant medicine, ie methods of HLA typing. Quality control is part of the quality management system. It consists of several components: validation, verification, internal quality control and external quality assessment. Each medical laboratory, including laboratories engaged in HLA typing, these elements must be applied to its routine operation. Validation is done before the introduction of methods and verifies whether the method is correct for the intended use. Verification is to verify that the validated method is used correctly in laboratory conditions. Internal quality control is based on an analysis of known positive and negative samples and evaluate the accuracy and precision of the whole analytical process. The external evaluation of the quality of the different laboratories analyze the same sample and the results are compared to each other. Key words: HLA typing, validation, verification, internal quality control, external quality assessment
|
|
|
Presenting results of software model checker via debugging interface
Kohan, Tomáš ; Šerý, Ondřej (advisor) ; Jančík, Pavel (referee)
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
|
|
|
Presenting results of software model checker via debugging interface
Kohan, Tomáš ; Šerý, Ondřej (advisor) ; Jančík, Pavel (referee)
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
|
|
|
Numerical modeling in groundwater contamination problems
Havlíková, Barbora ; Datel, Josef (advisor) ; Mls, Jiří (referee)
This bachelor thesis deals with numerical modelling of groundwater flow and contaminant transport. This thesis consists of two parts. In the first part are briefly described and compared basic methods, which are used for solving problems of groundwater flow and substance transport. Further more are set up initial and boundary conditions, which are an essential part of the compilation model. The second part deals with models from location Bzenec, where was the leakage of chlorinated aliphatic hydrocarbons. Models were created in purpose to describe the extent of contamination and spreading of contaminants and also to predict the further development of the pollution.
|
|
|
User-Defined XML-to-Relational Mapping
Kohan, Tomáš ; Mlýnková, Irena (advisor) ; Nečaský, Martin (referee)
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.
|
guest ::
