|
|
Automation of Verification Using Artificial Neural Networks
Fajčík, Martin ; Husár, Adam (referee) ; Zachariášová, Marcela (advisor)
The goal of this thesis is to analyze and to find solutions of optimization problems derived from automation of functional verification of hardware using artificial neural networks. Verification of any integrated circuit (so called Design Under Verification, DUV) using technique called coverage-driven verification and universal verification methodology (UVM) is carried out by sending stimuli inputs into DUV. The verification environment continuously monitors percentual coverage of DUV functionality given by the specification. In current context, coverage stands for measurable property of DUV, like count of verified arithemtic operations or count of executed lines of code. Based on the final coverage, it is possible to determine whether the coverage of DUV is high enough to declare DUV as verified. Otherwise, the input stimuli set needs to change in order to achieve higher coverage. Current trend is to generate this set by technique called constrained-random stimulus generation. We will practice this technique by using pseudorandom program generator (PNG). In this paper, we propose multiple solutions for following two optimization problems. First problem is ongoing modification of PNG constraints in such a way that the DUV can be verified by generated stimuli as quickly as possible. Second one is the problem of seeking the smallest set of stimuli such that this set verifies DUV. The qualities of the proposed solutions are verified on 32-bit application-specific instruction set processors (ASIPs) called Codasip uRISC and Codix Cobalt.
|
|
|
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)
|
|
|
Disarmament: the development of bilateral treaties between the USA and Russia
Svoboda, Lukáš ; Ondřej, Jan (advisor) ; Hýbnerová, Stanislava (referee)
The goal of this thesis was to map historical progress of disarmament agreements between Russian Federation and The United States of America from the end of the World War II, through the Cold War and ending in the present, formulated by the latest agreement NEW START made in 2010. This period of time includes rounds of negotiations about SALT, SALT II, INF agreement, through START I, START II, which never came in effect, ending with NEW START. Thesis is analyzing agreements not only via itself agreement's lines or proposals but also with their negotiations that led to formation of the agreements including brief historical background in which they were formatted. Rather bigger attention in this thesis is dedicated to the NEW START agreement which gained experience from past agreements. Thesis is divided into 5 chapters where the first chapter is dealing with theoretical delimits of terms which are necessary for sufficient understanding of the textual mater of these agreements. Other chapters are designed so that after every short introduction of the historical background is following analysis of the agreements or their particular links and their comparison with the previous agreements. Last chapter is focused on the issues about controlling the fulfillments of the agreements under the agreements...
|
|
|
The U.S.-Russian disarmament treaties and treaties on reduction of armaments and verification of their compliance
Šilha, Jakub ; Ondřej, Jan (advisor) ; Balaš, Vladimír (referee)
This thesis deals with the issue of verification of compliance of the treaties on reduction of armaments and disarmament concluded between the United States and the Soviet Union (now Russian Federation) in the period from the beginning of the Cold War until nowadays when the central point of the analysis is represented by the New START Treaty. In the background of study on the individual treaties, as well as of analysis of these bilateral treaties themselves, the thesis aspires to outline the most important aspects of the used verification regimes, their possible limits and apparent difficulties, and therefore contributes to a better understanding of the individual bilateral contractual approaches. The fundamental thought behind the thesis comes from the knowledge that the issue of verification usually means the feared point of discord in every, not only U.S.-Russian, negotiation between states which is to lead to conclusion of a new disarmament treaty. With respect to this circumstance, the thesis then aspires to prove that the above mentioned and recently concluded New START Treaty is the logical successor to a previously concluded disarmament treaties a that it is also based on experience with the previously applied verification regimes.
|
|
|
Comparison of the determination of hormones (Follicle stimulating hormone, Luteinizing hormone, Prolactin, Testosterone, Progesteron) by two analytical systems. Converting accredited method and its verification.
Kucejová, Soňa ; Martínková, Markéta (advisor) ; Mrízová, Iveta (referee)
Analytical system ARCHITECT i2000SR was verified according to requirements of ÚLBLD VFN and 1. LF UK laboratory in Prague. Repeatability, intermediate precision, and measurement uncertainty were determined as performance parameters for verification of analytical assays for testosterone, progesterone, luteinizing hormone, follicule stimulating hormone and prolactin. Results of Lyphochek control samples, which were measured, were consistent with values given by manufacture. Repeatability: coefficients of variation for testosterone Lyphochek 1 6,81%, for Lyphochek 3 6,40%, progesterone 2,4% and 1,8%, luteinizing hormone 5,38% and 1,89%, follicle stimulating hormone 5,12% and 3,24% prolactin 1,45% a 1,83%. Intermediate precision: coefficients of variation for testosterone Lyphochek 1 6,02%, Lyphochek 2 3,60%, Lyphochek 3 3,07%, progesterone 7,9%, 4,9% and 5,8%, luteinizing hormone 4,50%, 5,51% and 5,83%, follicle stimulating hormone 4,00%, 3,72% and 4,87%, prolactin 4,60%, 4,20% and 5,00%. Measurement uncertainty: testosterone 6,02%, progesterone 7,9%, luteinizing hormone 5,83%, follicle stimulating hormone 4,87%, prolactin 5,00%. Analytical System Architect i2000SR was compared with previously used ADVIA Centaur system to find out, whether it is possible to convert the method Centaur Testosterone,...
|
|
|
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.
|
|
|
Verification of Textual Use-Cases
Vinárek, Jiří ; Šimko, Viliam (advisor) ; Hauzar, David (referee)
The aim of this thesis is to create a tool for formal verification of systems specified using textual use- cases. The tool should allow for automated verification of temporal invariants specified in temporal logic (CTL and LTL formulae). The textual specification is transformed to a formal model that is verified using the NuSMV symbolic model-checker. Potential errors are shown to the user in the form of an HTML report. Using this feedback, the user is able to iteratively develop valid textual use-case specifications. The tool's architecture should be focused on reusability of its components and extensibility. Powered by TCPDF (www.tcpdf.org)
|
|
|
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 issue of the revision corrected wiring residential building
Štefek, Roman ; Janda, Marcel (referee) ; Veselka, František (advisor)
Bachelor’s thesis deals with the verification of electrical installations in residential buildings. The task of the thesis is to get acquainted with the requirements of the regulations with a focus on Czech technical standard CSN 33 2000-6, CSN 33 1500 and follow-up. Specifically, the information gathered is used to the implementation of the review installations in renovated apartment building. The aim is to apply the theoretical knowledge and information for the practical verification of the electrical installation.
|
|
|
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.
|
guest ::
