Název: Automatická formální verifikace korektnosti programů v nástrojích SDV, Copper a podobných
Překlad názvu: Automated Formal Verification of Program Correctness Using SDV, Copper, or Similar Tools
Autoři: Kovalič, Peter ; Šimáček, Jiří (oponent) ; Vojnar, Tomáš (vedoucí práce)
Typ dokumentu: Bakalářské práce
Rok: 2010
Jazyk: cze
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [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.
Klíčová slova: BLAST; Copper; Ext2Fsd; model checking; ovladač; ovládač souborového systému; PREfast; static driver verifier; statická analýza; verifikace; Windows driver kit; BLAST; Copper; driver; Ext2Fsd; file systém driver; model checking; PREfast; static analysis; static driver vernier; verification; Windows driver kit

Instituce: Vysoké učení technické v Brně (web)
Informace o dostupnosti dokumentu: Plný text je dostupný v Digitální knihovně VUT.
Původní záznam: http://hdl.handle.net/11012/55994

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-567274


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Vysoké učení technické v Brně
Vysokoškolské kvalifikační práce > Bakalářské práce