Detail práce

Bounded model checking v nástroji Java PathFinder

Diplomová práce Student: Dudka Vendula Akademický rok: 2007/2008 Vedoucí: Křena Bohuslav, Ing., Ph.D.
Název anglicky
Bounded Model Checking Using Java PathFinder
Jazyk práce
český
Abstrakt

Diplomová práce je věnovaná aplikaci formální metody bounded model checking pro automatickou opravu chyb. Oprava se specializuje na chyby spojené se souběžností. Práce je zaměřena na programy napsané v jazyce Java, a proto pro verifikační metodu byl zvolen model checker Java Pathfinder, který je určen pro Java programy. Vlastní verifikační metoda spočívá v aplikaci strategie pro navigaci stavovým prostorem do místa verifikace. Z daného místa je spuštěn bounded model checking pro ověření opravy. Navigace stavovým prostorem je implementována pomocí strategie record&replay trace. Pro aplikaci bounded model checkingu jsou implementovány další parametry a moduly pro verifikaci speciálních vlastností systému, které ověřují koreknost opravy chyby. Bounded model checking se provádí v okolí opravy.

Klíčová slova

Model Checking, Java PathFinder, Bounded model checking, verifikace, Record&Replay trace, automatická oprava, souběžnost, ověřování opravy

Ústav
Ústav inteligentních systémů FIT VUT v Brně
Studijní program
Informační technologie, obor Počítačová grafika a multimédia
Soubory
Stav
obhájeno, hodnocení B
Obhajoba
17. června 2008
Oponent
Češka Milan, prof. RNDr., CSc.
Komise
Meduna Alexander, prof. RNDr., CSc. (UIFS FIT VUT), předseda
Černocký Jan, prof. Dr. Ing. (UPGM FIT VUT), člen
Fučík Otto, doc. Dr. Ing. (UPSY FIT VUT), člen
Kršek Přemysl, doc. Ing., Ph.D. (UPGM FIT VUT), člen
Sochor Jiří, prof. Ing., CSc. (FI MUNI), člen
Zemčík Pavel, prof. Dr. Ing. (UPGM FIT VUT), člen
Citace
DUDKA, Vendula. Bounded model checking v nástroji Java PathFinder. Brno, 2008. Diplomová práce. Vysoké učení technické v Brně, Fakulta informačních technologií. 2008-06-17. Vedoucí práce Křena Bohuslav. Dostupné z: https://www.fit.vut.cz/study/thesis/6443/
BibTeX 
@mastersthesis{FITMT6443,
    author = "Vendula Dudka",
    type = "Diplomov\'{a} pr\'{a}ce",
    title = "Bounded model checking v n\'{a}stroji Java PathFinder",
    school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
    year = 2008,
    location = "Brno, CZ",
    language = "czech",
    url = "https://www.fit.vut.cz/study/thesis/6443/"
}

Závěrečné práce

Nahoru