Diplomová práce

Akcelerace procesu verifikace pomocí grafické karty

GPU accelerated LTL Model Checking

Bc. Tomáš Lamr, učo 140423
Anotace

Programové systémy zastávají čím dál více úloh, ve kterých není přípustné jejich selhání. Například při řízení letového provozu by chyba programu mohla ohrozit nejen majetek leteckých společností ale i zdraví a životy cestujících. Z toho důvodu jsou vyvíjeny metody formální verifikace, které matematicky dokáží korektnost, tj. bezchybnost daného programového vybavení. Jedním z nejpoužívanějších přístupů …více

Abstract

Modern computer systems plays important role that affects our lifes in many cases. For example, if a system for air traffic control would fail, there could be many losses on possession of Air transport companies, or even passengers could be in danger. These systems needs to be verified. It's important to be sure, that there are no bugs inside of them. Many methods of formal verification arose, one …více

Klíčová slova
model-checking gpu cuda map mas maximal accepting predecessors maximal accepting successors divine ltl
Zadání práce
Cílem práce je zvážit možnosti akcelerace algoritmů pro detekci akceptujících cyklů pomocí soudobých grafických karet. Vybranou techniku implementovat a experimentálně vyhodnotit na modelech z databáze BEEM. Součástí práce bude diskuze o omezeních implementované techniky a případné shrnutí výhod a nevýhod jiných přístupů. Implementace bude využívat stávající verzi verifikačního nástroje DiVinE.
Administrativní informace
Práce zkontrolována:
1. 6. 2009 10:52, prof. RNDr. Jiří Barnat, Ph.D., učo 3496
Plný text práce
940,3 KB / soubor PDF
Jazyk práce
čeština čeština
Termín obhajoby
3. 7. 2009
Práce byla úspěšně obhájena

Vedoucí

prof. RNDr. Jiří Barnat, Ph.D., učo 3496
KTP FI MU

Oponent

doc. RNDr. Milan Češka, Ph.D.
abs FI MU
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Aplikovaná informatika
Obor

Práce na příbuzné téma

Seznam prací, které mají shodná klíčová slova.

Podobné práce
 
Název
Vložil
Vloženo
Práva
Archiv závěrečné práce Tomáš Lamr FI N-AP AP, učo 140423 lx49p/7
Lamr, T.
21. 5. 2009
Složky
Soubory
Anotace anglicky annotation_english.txt
Lamr, T.
21. 5. 2009
Anotace česky annotation.txt
Lamr, T.
21. 5. 2009
CD cd.tar.gz
Lamr, T.
21. 5. 2009
Diplomová práce - Tomáš Lamr diplomka.pdf
Lamr, T.
21. 5. 2009
Klíčová slova keywords.txt
Lamr, T.
21. 5. 2009
posudek_oponenta.pdf
Češka, M.
24. 6. 2009

  • Přidání souboru

    Soubor nebo složku lze nahrát pomocí tlačítka Přidat.

  • Další operace se soubory

    Podrobnosti lze zjistit označením příslušného řádku.

  • Pohled pro experty

    Pro častou práci je možné zvolit režim Více možností.

  • Vyhledávání souborů

    Vyhledávaný výraz můžete zadat přímo do adresního řádku.

  • Rychlý přístup k souborům

    Pomocí funkce Nedávné je možné se rychle vrátit k právě prohlíženým souborům. Oblíbené soubory je také možné označit Hvězdičkou.