Detail práce

Ověřování parametrických vlastností nad záznamy běhů programů

Diplomová práce Student: Čaládi Filip Akademický rok: 2021/2022 Vedoucí: Smrčka Aleš, Ing., Ph.D.
Název anglicky
Parametric Properties for Log Checker
Jazyk práce
český
Abstrakt

Plogchecker 2.0 je nástroj zameraný na verifikáciu užívatelom definovaných vlastností nad sekvenciou udalostí generovaných programom. Implementácia tohoto nástroja stavá hlavne na už implementovanom nástroji Plogchecker. Hlavná mýšlienka týchto nástrojov je, že užívatel musí špecifikovať želané vlastnosti (parametrické alebo neparametrické), sprístupniť záznam behu programu verifikačnému nástroju a konečne prenechať analýzu na tento nástroj. Výstup analýzy je report o porušení špecifikovaných vlastností spolu so sekvenciami udalostí, ktoré spôsobili chybu. Táto práca predstavuje nový algoritmus , ktorý optimalizuje spracovanie sekvenie udalostí nad užívatelom definovanými vlastnosťami. Táto optimalizácia sa zameriava ako na škálovatelnosť tak aj presnosť. Ďalej, je pridaná podpora pre rôzne dátové typy parametrov, ako napríklad reťazec, číslo, dátum a čas. Nakoniec, táto práca ponúka jednoduchší a pohodlnejší spôsob vytvárania parametických vlastností. Počas experimentovania bolo ukázané, že Plogchecker 2.0 je schopný väčšej škálovatelnostia presnosti.

Klíčová slova

verifikácia za behu, parametrické vlastnosti, neparametrické vlastnosti, rozšírené regulárne výrazy, konečné automaty, golang, grok, garbage collecting

Ústav
Studijní program
Informační technologie a umělá inteligence, specializace Verifikace a testování software
Soubory
Stav
obhájeno, hodnocení B
Obhajoba
17. června 2022
Oponent
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 B.

Otázky u obhajoby
  1. V práci jsou srovnány nástroje plogchecker (python) a plogchecker2 (go) z hlediska času a spotřeby paměti. Závěry srovnání však nemusí nutně znamenat, že je navržená metoda založená na tabulkách efektivnější než předchozí metoda založená na konečných automatech. Srovnejte důkladněji efektivitu pouze těchto dvou metod (např. je srovnejte z hlediska velikosti automatů a z hlediska velikosti tabulek a jejich relací).
  2. Diskutujte použitelnost Vašeho nástroje pro monitorování výkonnosti programů (např. monitorování doby odezvy na požadavky na REST API).
  3. Na jakých benchmarcích jste prováděl vaše měření?
  4. Jak přesně jsou tabulky provázány s automaty?
  5. Jaké sekvence jsou v uváděném logu?
Komise
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT), předseda
Češka Milan, doc. RNDr., Ph.D. (UITS FIT VUT), člen
Meduna Alexander, prof. RNDr., CSc. (UIFS FIT VUT), člen
Peringer Petr, Dr. Ing. (UITS FIT VUT), člen
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT), člen
Veselý Vladimír, Ing., Ph.D. (UIFS FIT VUT), člen
Citace
ČALÁDI, Filip. Ověřování parametrických vlastností nad záznamy běhů programů. Brno, 2022. Diplomová práce. Vysoké učení technické v Brně, Fakulta informačních technologií. 2022-06-17. Vedoucí práce Smrčka Aleš. Dostupné z: https://www.fit.vut.cz/study/thesis/23298/
BibTeX
@mastersthesis{FITMT23298,
    author = "Filip \v{C}al\'{a}di",
    type = "Diplomov\'{a} pr\'{a}ce",
    title = "Ov\v{e}\v{r}ov\'{a}n\'{i} parametrick\'{y}ch vlastnost\'{i} nad z\'{a}znamy b\v{e}h\r{u} program\r{u}",
    school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
    year = 2022,
    location = "Brno, CZ",
    language = "czech",
    url = "https://www.fit.vut.cz/study/thesis/23298/"
}
Nahoru