Original title: Automatická formální verifikace korektnosti programů v nástrojích SDV, Copper a podobných
Translated title: Automated Formal Verification of Program Correctness Using SDV, Copper, or Similar Tools
Authors: Kovalič, Peter ; Šimáček, Jiří (referee) ; Vojnar, Tomáš (advisor)
Document type: Bachelor's theses
Year: 2010
Language: cze
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [cze] [eng]
Tato práce se věnuje verifikaci ovládačů. Používají se při tom model checkery, hlavní z nich je Static Driver Verifier. Pomocí něj se kontroluje zvolený ovládač Ext2Fsd. Patří do skupiny ovládačů souborových systémů. Kontrola probíhá podle zadaných pravidel, které nesmí ovládač porušovat. Cílem práce bylo vybraný ovládač verifikovat pomocí zvoleného nástroje. Ve výsledcích bylo dosaženo stavu, kdy se ve verifikovaném ovládači objevili všechny tři dostupné možnosti výsledku ovládač splňoval některá pravidla, některá odhalily jeho chyby a jiné nebyly aplikovatelné. Na konci této práce se nachází ještě kapitola, věnována dalšímu model checkeru, s názvem Copper, která poskytuje základní poznatky o tomto nástroji. 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.
Keywords: BLAST; Copper; driver; Ext2Fsd; file systém driver; model checking; PREfast; static analysis; static driver vernier; verification; Windows driver kit; BLAST; Copper; Ext2Fsd; model checking; ovladač; ovládač souborového systému; PREfast; static driver verifier; statická analýza; verifikace; Windows driver kit

Institution: Brno University of Technology (web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library.
Original record: http://hdl.handle.net/11012/55994

Permalink: http://www.nusl.cz/ntk/nusl-567274


The record appears in these collections:
Universities and colleges > Public universities > Brno University of Technology
Academic theses (ETDs) > Bachelor's theses