Detail práce
Ověřování parametrických vlastností nad záznamy běhů programů
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.
verifikácia za behu, parametrické vlastnosti, neparametrické vlastnosti, rozšírené regulárne výrazy, konečné automaty, golang, grok, garbage collecting
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.
- 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í).
- Diskutujte použitelnost Vašeho nástroje pro monitorování výkonnosti programů (např. monitorování doby odezvy na požadavky na REST API).
- Na jakých benchmarcích jste prováděl vaše měření?
- Jak přesně jsou tabulky provázány s automaty?
- Jaké sekvence jsou v uváděném logu?
Č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
@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/" }