Detail práce

Static Analysis in the Frama-C Environment Focused on Deadlock Detection

Bakalářská práce Student: Dacík Tomáš Akademický rok: 2019/2020 Vedoucí: Vojnar Tomáš, prof. Ing., Ph.D.
Název česky
Statická analýza v prostředí Frama-C zaměřená na detekci uváznutí
Jazyk práce
anglický
Abstrakt

Tato práce se zabývá návrhem nového statického analyzátoru pro detekci uváznutí, implementovaného jako plugin platformy Frama-C. Kromě samotného algoritmu pro detekci uváznutí představuje také odlehčené řešení, které umožňuje využít platformu Frama-C pro analýzu vícevláknových programů s využitím analyzátorů Frama-C podporujících pouze sekvenční programy. Výsledky experimentů ukazují, že implementovaný nástroj je schopný analyzovat reálné programy s vysokou přesností. Pro demonstraci další rozšiřitelnosti je představeno experimentální rozšíření umožňující detekovat také časově závislé chyby nad daty.

Klíčová slova

uváznutí, časově závislá chyba nad daty, statická analýza, abstraktní interpretace, analýza vícevláknových programů, Frama-C

Ústav
Ústav inteligentních systémů FIT VUT v Brně
Studijní program
Informační technologie
Soubory
Stav
obhájeno, hodnocení A
Obhajoba
10. července 2020
Oponent
Holík Lukáš, doc. Mgr., Ph.D.
Průběh obhajoby

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ázky 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 A.

Otázky u obhajoby
  1. Je počet cest na hranách grafu omezený i v případě rekurzivních programů, kde je počet rekurzivních volání neomezený? Jak to?
  2. Existují možné alternativy k nástroji EVA, který by byly rychlejší/přesnější ... ?
  3. Jak by se dal Váš přístup smysluplně vylepšit co do efektivity, přesnosti nebo obecnosti?
Komise
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT), předseda
Kekely Lukáš, Ing., Ph.D. (UPSY FIT VUT), člen
Křivka Zbyněk, Ing., Ph.D. (UIFS FIT VUT), člen
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT), člen
Španěl Michal, Ing., Ph.D. (UPGM FIT VUT), člen
Citace
DACÍK, Tomáš. Static Analysis in the Frama-C Environment Focused on Deadlock Detection. Brno, 2020. Bakalářská práce. Vysoké učení technické v Brně, Fakulta informačních technologií. 2020-07-10. Vedoucí práce Vojnar Tomáš. Dostupné z: https://www.fit.vut.cz/study/thesis/22928/
BibTeX 
@bachelorsthesis{FITBT22928,
    author = "Tom\'{a}\v{s} Dac\'{i}k",
    type = "Bakal\'{a}\v{r}sk\'{a} pr\'{a}ce",
    title = "Static Analysis in the Frama-C Environment Focused on Deadlock Detection",
    school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
    year = 2020,
    location = "Brno, CZ",
    language = "english",
    url = "https://www.fit.vut.cz/study/thesis/22928/"
}

Závěrečné práce

Nahoru