Detail práce

Pokrytelnosti pro paralelní programy

Diplomová práce Student: Holíková Lenka Akademický rok: 2014/2015 Vedoucí: Holík Lukáš, doc. Mgr., Ph.D.
Název anglicky
Coverability for Parallel Programs
Jazyk práce
český
Abstrakt
Tato diplomová práce se zabývá automatickou verifikací systémů s paralelně běžícími procesy. Práce diskutuje existující metody a možnosti jejich optimalizace. Stávající techniky jsou založeny na hledání induktivního invariantu (například pomocí techniky zjemňování
abstrakce řízené protipříklady (CEGAR)). Efektivnost metod závisí na velikosti nalezeného invariantu. V rámci této diplomové práce jsme nalezli možnost zlepšení metod díky zaměření se na hledání invariantů minimální velikosti. Naimplementovali jsme nástroj, který zajišťuje
prohledávání prostoru invariantů systému. Naše experimentální výsledky ukazují, že mnoho existujících systémů užívaných v praxi má skutečně mnohem menší invarianty než ty, které lze nalézt stávajícími metodami. Závěry a výsledky této práce budou sloužit jako základ budoucího výzkumu, jehož cílem bude navržení optimální metody pro vypočítání malých invariantů paralelních systémů.
Klíčová slova

Paralelní systémy, formální verifi kace, Petriho sítě, pokrytelnost, abstrakce, dobře kvasi-uspořádané přechodové systémy.

Ústav
Studijní program
Informační technologie, obor Bioinformatika a biocomputing
Soubory
Stav
obhájeno, hodnocení A
Obhajoba
24. června 2015
Oponent
Průběh obhajoby

Studentka nejprve prezentovala výsledky, kterých dosáhla v rámci své práce. Komise se poté seznámila s hodnocením vedoucího a posudkem oponenta práce. Studentka následně odpověděla 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í studentky na položené otázky rozhodla práci hodnotit stupněm "A".

Otázky u obhajoby
  1. Vysvětlete, zda jsou opravdu v zápisu Algoritmu 5 výše uvedené chyby, a případně je korigujte.
  2. Vysvětlete, jak souvisí Váš text v prvním pojmenovaném odstavci sekce 7.6 se vztahem 4.10.
  3. Je-li to rozsahově možné (rozsah v rámci 1 slajdu), uveďte pseudokód odpovídající druhému pojmenovanému odstavci v sekci 7.6.
  4. Platí vždy, že práce s menšími invarianty povede k efektivnější verifikaci?
  5. Jak souvisí růst světové populace s rychlostí počítačů (viz první věta úvodu)?
Komise
Sekanina Lukáš, prof. Ing., Ph.D. (UPSY FIT VUT), předseda
Bartík Vladimír, Ing., Ph.D. (UIFS FIT VUT), člen
Holík Lukáš, doc. Mgr., Ph.D. (UITS FIT VUT), člen
Martínek Tomáš, doc. Ing., Ph.D. (UPSY FIT VUT), člen
Šaloun Petr, doc. RNDr., Ph.D. (VŠB-TUO), člen
Zbořil František, doc. Ing., Ph.D. (UITS FIT VUT), člen
Citace
HOLÍKOVÁ, Lenka. Pokrytelnosti pro paralelní programy. Brno, 2015. Diplomová práce. Vysoké učení technické v Brně, Fakulta informačních technologií. 2015-06-24. Vedoucí práce Holík Lukáš. Dostupné z: https://www.fit.vut.cz/study/thesis/17241/
BibTeX
@mastersthesis{FITMT17241,
    author = "Lenka Hol\'{i}kov\'{a}",
    type = "Diplomov\'{a} pr\'{a}ce",
    title = "Pokrytelnosti pro paraleln\'{i} programy",
    school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
    year = 2015,
    location = "Brno, CZ",
    language = "czech",
    url = "https://www.fit.vut.cz/study/thesis/17241/"
}
Nahoru