|
|
Automated Formal Verification of Program Correctness Using SDV, Copper, or Similar Tools
Kovalič, Peter ; Šimáček, Jiří (referee) ; Vojnar, Tomáš (advisor)
This thesis is concerning about verification of drivers. Principally is focused on model checking tools, from which the Static Driver Verifier is the most important. A driver Ext2Fsd is checked by this program. This driver belongs to group of file system drivers. Control is driven by entered rules, which the driver must not violate. The aim of this thesis was to verify chosen driver by selected tool. The results have covered all three types of verification´s end. There were rules that driver passed, that driver violated and also that driver didn´t accept. The final chapter of work is about another model checking tool Copper. It offers the basic knowledge about this program.
|
|
|
Genomic Data Mining Techniques
Jaša, Petr ; Křivka, Zbyněk (referee) ; Burgetová, Ivana (advisor)
First of all, this thesis sets itself a goal to introduce some common technics for datamining in genomics and as a next step to implement own algorithm like algorithm BLAST. In the concrete, this work is pointed to sequences of DNA. The DNA sequence contains in itself genetic information, which is template for living organism. For explanation this information can be used number of technics. This paper describes algorithm Fasta and algorithms from BLAST family. With these algorithms, it is possible to gain a lot of important information even about such DNA sequences, where only primary structure is known. Principle of these algorithms is based on alignments of one query sequence, which we want to obtain some information from, with many sequences stored in database. According to result alignment, it is possible to determine many features of the query sequence.
|
|
|
Homology search using digital signal processing methods
Kamar, Yana ; Jugas, Robin (referee) ; Maděránková, Denisa (advisor)
Thesis includes the theoretical introduction to molecular biology and genetics on the necessary level, including a description of the structure of DNA and the homologous gene. Described are fixed and physic-chemical kinds of nucleotide mapping, methods for processing digital signals. Numerical representations of genes that were programmed in MATLAB: unwrapped and accumulated phases, density vectors. Using the unwrapped phase and density vectors with windows of different lengths was performed CDS searching in the entire genome by calculation metric distances (euclidean and canberian) and correlation. Also, using the metric distances, a homologous gene was found in more or less similar bacterial genomes. The result is the approximate threshold of distance (euclidean and canberian) using to find homologous genes in genome.
|
|
|
Character-based methods for DNA barcoding
Kalianková, Kateřina ; Sedlář, Karel (referee) ; Maděránková, Denisa (advisor)
This work deals with character-based DNA barcoding. DNA barcoding and character-based DNA barcoding methods are described in the introduction. Another part contains information of method CAOS (Characteristic Attributes Organization), method BLOG (Barcoding with LOGic) and method BLAST. Programs are described in the practical part. The end contains results.
|
|
|
Stress-strain analysis of the thin wall structure subjected to impact load
Tatalák, Adam ; Peč, Michal (referee) ; Návrat, Tomáš (advisor)
This master thesis deals with stress-strain analysis of simplified model of the thin wall transformer case subjected to impact load of electrical blast. Electrical blast is replaced by chemical blast (detonation of high explosive). The problem is solved using computational modeling utilizing the Finite Element Method (FEM) and LS-DYNA solver. After the introduction where detonation and shock wave propagation is explained the analytical approach is presented. This approach serves to results verification. In the next chapter is conducted research of applicable methods from which ALE method is chosen. In preliminary study is performed the mesh size analysis that is focused on finding the size of element which is both computational effective and gives accurate results. Next the infulence of input conditions (shape, location and parametres of high explosive, location of detonation point, boundary conditions) on distribution and time progress of pressure is investigated. Then influence of the opening on upper side of the case on overall pressure redistribution and strain and stress of the case is analysed. The stress-strain analysis of the case´s door which are connected to case by various types of contact models is performed as well as stiffness analysis of these types of contact.
|
|
|
Automated Formal Verification of Program Correctness Using SDV, Copper, or Similar Tools
Kovalič, Peter ; Šimáček, Jiří (referee) ; Vojnar, Tomáš (advisor)
This thesis is concerning about verification of drivers. Principally is focused on model checking tools, from which the Static Driver Verifier is the most important. A driver Ext2Fsd is checked by this program. This driver belongs to group of file system drivers. Control is driven by entered rules, which the driver must not violate. The aim of this thesis was to verify chosen driver by selected tool. The results have covered all three types of verification´s end. There were rules that driver passed, that driver violated and also that driver didn´t accept. The final chapter of work is about another model checking tool Copper. It offers the basic knowledge about this program.
|
|
|
Analysis of Genomic Data with the Assistance of Algorithm BLAST
Křížová, Martina ; Burgetová, Ivana (referee) ; Jaša, Petr (advisor)
This Bachelor Thesis describes analysis of genomic data with assistance of algorithm BLAST. In theoretic part, it describes genomes, their importance and structure. In this thesis, you can find a description of algorithm BLAST, Smith-Waterman and Needleman-Wunsch and with algorithm BLAST connected Karlin-Altschul statistics. This thesis is discussing types of databases such as spatial, deductive and relational which store genomic data. Second part is concerned with design and implementation of application which use mentioned algorithm and database Oracle 10g R2. Testing and confrontation output of algorithm is also a part of this work.
|
|
|
Application for Alignment of DNA Parts
Kašpárek, Tomáš ; Žák, Jakub (referee) ; Rozman, Jaroslav (advisor)
This thesis deals with DNA sequences alignment methods with focus on execution speed of given task and its optimality. The outcome of this thesis results in multiple programs, which presents DNA alignment algorithms and their versions programmed with OpenCL libraries, which are optimized on calculation rate. Text of this thesis apprises reader with DNA alignment problematic and its importance in biology. Further, algorithms for DNA alignment and options of their speed-up using libraries like CUDA or OpenCL are presented.
|
|
|
Approximate String Matching Algorithm Implementation in FPGA
Pařenica, Martin ; Martínek, Tomáš (referee) ; Fučík, Otto (advisor)
This paper describes sequence alignment algorithms of nucleotide sequences. There are described pairwise alignment algorithms using database search or dynamic programming. Then in the paper is description of dynamic programming for multiple sequences and algorithm that builds phylogenetic trees. At the end of the first part of the paper is the description of technology FPGA. In the second part that is more practical is described implemntation of the choosen one algorithm. This part includes also examples of some multiple alignments.
|
|
|
Techniques for Comparing Biological Sequences
Sladký, Roman ; Křivka, Zbyněk (referee) ; Burgetová, Ivana (advisor)
This work presents the building up of basic biological units DNA, RNA and proteins as well as their function. Provided data are kept in biological databases which are connected worldwide to supply preferable communication along with all kinds of available information to be used in the scientific research. The secret of alive is hidden in genes coded in sequences of nucleotides. Genes enable the creation of proteins which are made of sequences of amino-acids. The wide-spread methods of comparing these sequences are FASTA and BLAST algorithms. Their base is used for the PSProt program which is described in this work. PSProt program is the tool for comparing the sequences of proteins. First it is necessary to synthesise the protein from the DNA oligonucleotide because it codes the surveyed protein. The most similar proteins are searched out by heuristic of hitpoints, then their final score that is essential for aligning is modified by semiglobal alignment algorithm.
|
guest ::
