Detail práce
Nástoj pro abstraktní regulární stromový model checking
Formálna verifikácia sa zaoberá dokazovaním korektnosti systému podľa daných špecifikácií.Jej potrebu znásobuje stále väčšia rozšírenosť počítačov a neustály rast zložitosti aj rozsiahlosti vyvíjaných systémov. Cieľom tejto práce je implementácia nástroja formálnejverifikácie abstraktný regulárny stromový model checking (ARTMC) nad knižnicou VATA. Pre dosiahnutie tohto cieľa bolo potrebné rozšíriť knižnicu VATA o konečné stromové prevodníky,abstrakcie stromových automatov a integrovať ich spolu s nástrojom ARTMC doknižnice VATA.
abstraktný regulárny stromový model checking, ARTMC, stromový automat, stromový prevodník, abstrakcia, VATA
Student nejprve prezentoval výsledky, kterých dosáhl v rámci své práce. Komise se poté seznámila s hodnocením vedoucího a posudkem oponenta práce. Student následně odpověděl na otázku oponenta a na další otázky přítomných. Komise se na základě posudku oponenta, hodnocení vedoucího, přednesené prezentace a odpovědí studenta na položené otázky rozhodla práci hodnotit stupněm "D".
- Co způsobuje, že verifikační smyčka v mnoha případech skončila po jednom kroce a často bez vytváření nových predikátů i když z pohledu teorie to tak být nemá.
Grézl František, Ing., Ph.D. (UPGM FIT VUT), člen
Hanáček Petr, doc. Dr. Ing. (UITS FIT VUT), člen
Kořenek Jan, doc. Ing., Ph.D. (UPSY FIT VUT), člen
Veselý Vladimír, Ing., Ph.D. (UIFS FIT VUT), člen
@bachelorsthesis{FITBT19056,
author = "Patrik Mr\'{a}z",
type = "Bakal\'{a}\v{r}sk\'{a} pr\'{a}ce",
title = "N\'{a}stoj pro abstraktn\'{i} regul\'{a}rn\'{i} stromov\'{y} model checking",
school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
year = 2017,
location = "Brno, CZ",
language = "czech",
url = "https://www.fit.vut.cz/study/thesis/19056/"
}