Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
bakalářská práce
Autor práce: Bc. Samuel Ján Mucha
Ak. rok: 2024/2025
Vedoucí: Ing. Jan Fiedor, Ph.D.
Oponent: Ing. David Hudák
Redundancia testov v modeloch Simulink predstavuje významnú výzvu pre efektívnosť overovania softvéru. Táto práca skúma detekciu izomorfizmu podgrafov pomocou algoritmu VF3, adaptovaného a implementovaného v rámci vlastného reťazca nástrojov BLADE-BALROG-BALIN. BLADE zjednodušuje modelovanie modelov Simulink, BALROG spracováva konverziu grafov pre internú reprezentáciu v NetworkX a BALIN vykonáva VF3. Benchmarking na grafoch podobných Simulinku demonštruje takmer kubickú škálovateľnosť priemernej doby behu a efektívne odmietnutie neizomorfizmu. Počiatočné testy modelu BLADE potvrdili správnosť. Tento výskum zavádza reťazec nástrojov a poskytuje sľubné dôkazy o tom, že VF3 dokáže efektívne znížiť redundanciu v testovaní založenom na modeloch Simulink, čím sa zvyšuje efektívnosť overovania softvéru.
Podgrafový Izomorfizmus, Algoritmus VF3, Simulink, BLADE, NetworkX, Analýza Modelov, Atribuované orientované grafy
Termín obhajoby
17.06.2025
Výsledek obhajoby
obhájeno (práce byla úspěšně obhájena)
Klasifikace
A
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 k obhajobě
Jazyk práce
angličtina
Fakulta
Fakulta informačních technologií
Ústav
Ústav inteligentních systémů
Studijní program
Informační technologie (BIT)
Složení komise
doc. RNDr. Milan Češka, Ph.D. (předseda) Ing. Radek Kočí, Ph.D. (člen) Ing. Šárka Květoňová, Ph.D. (člen) Ing. David Bařina, Ph.D. (člen) Ing. Marta Jaroš, Ph.D. (člen)
Posudek vedoucíhoIng. Jan Fiedor, Ph.D.
Jde o excelentní práci po všech stránkách, od návrhu a formalizace modifikovaného VF3 algoritmu, přes jeho generickou a jednoduše rozšířitelnou implementaci, až po detailní evaluaci provedenou navíc na netriviální sadě reálných MATLAB/Simulink modelů společnosti Honeywell. Pro reprodukovatelnost evaluace navíc student vytvořil open-source knihovnu BLADE pro MATLAB/Simulink, jenž je již nyní s výhodou využívána v dalších pracích řešených na FIT VUT i FI MUNI a také výzkumnou skupinou VeriFIT. Po výborných výsledcích aplikace práce ve společnosti Honeywell se navíc připravuje její aplikace na další rozsáhlé sady MATLAB/Simulink modelů.
S přihlédnutím k excelentním dosaženým výsledkům navrhuji zvážit ocenění práce.
Cílem práce bylo aplikovat NP-úplný problém izomorfismu podgrafů na praktický problém minimalizace testů pro MATLAB/Simulink modely. Student nastudoval nejnovější (a nejkomplexnější) variantu VF algoritmu pro izomorfismus podgrafů, algoritmus VF3, a implementoval ho jako obecný a jednoduše rozšířitelný algoritmus pro grafovou knihovnu NetworkX. Tato obecná implementace je nezávislá na sémantických kontrolách a kategorizaci uzlů grafu, jenž je typicky potřeba definovat pro každý typ analyzovaných grafů zvlášť. Dále vytvořil tři varianty sémantických kontrol a kategorizace uzlů grafu vhodných pro porovnávání MATLAB/Simulink modelů.
Práce vyžadovala důkladné studium a pochopení algoritmu VF3, včetně jeho předchůdců, jeho adaptaci pro účely analýzy grafů reprezentujících MATLAB/Simulink modely, a nakonec vytvoření nástroje schopného analyzovat reálné modely společnosti Honeywell pro účely minimalizace testů, jenž tyto modely využívají. Práci tedy hodnotím jako velmi náročnou jak z pohledu teorie, tak samotné realizace.
Student aktivně vyhledával relevantní zdroje informací a využíval je k řešení bakalářské práce. Z důvodu úzkého zaměření práce si vystačuje technická zpráva s malým množstvím studijních materiálů. Jádro práce tvoří několik vědeckých článků rozebírajících algoritmus VF3 a jeho varianty, jenž musel student do detailu prostudovat a pochopit jak pro účely implementace, tak pro formalizaci jeho vlastní modifikace algoritmu VF3, kterou lze aplikovat na grafy reprezentující MATLAB/Simulink modely.
Student byl velmi aktivní a své řešení pravidelně konzultoval jak s vedoucím, tak s technických vedoucím práce. Veškeré potřebné modifikace algoritmu VF3 navrhl sám a byly podrobně diskutovány s oběma vedoucími práce. Pro evaluaci práce navrhl student vlastní sadu testů, využívajících veřejnou knihovnu BLADE pro MATLAB/Simulink, kterou sám vytvořil o semestr dříve. Následně práci úspěšně otestoval na reálných příkladech dodaných technickým vedoucím ze společnosti Honeywell.
Práce byla dokončena v dostatečném předstihu a průběžně konzultována. Poslední týdny byly využity k rozšiřování evaluace o dodatečné testovací scénáře a vylepšování formalizace algoritmu VF3 a v něm provedených úprav, což nadále zvyšovalo již tak velmi vysokou kvalitu práce.
Vytvořená implementace je veřejně k dispozici na GitLab serveru výzkumné skupiny VeriFIT. Student tuto implementaci vyhodnotil jak z pohledu průměrné časové složitosti algoritmu při aplikaci na MATLAB/Simulink modely, tak z pohledu využití v praxi, kde analyzoval téměř 1000 MATLAB/Simulink modelů společnosti Honeywell, detekoval 51% redundantních modelů, a výrazně tak zredukoval počet testů spouštěných při regresním testování jednoho z interních nástrojů společnosti Honeywell. Jelikož interní modely společnosti Honeywell nemohou externí uživatelé použít k ověření implementovaného algoritmu, vytvořil student také knihovnu BLADE pro MATLAB/Simulink, jenž umožňuje vytvářet veřejně přístupné MATLAB/Simulink modely analyzovatelné (nejen) tímto algoritmem, čímž položil základ pro několik dalších (již nyní obhajovaných) bakalářských a diplomových prací.
Známka navržená vedoucím: A
Posudek oponentaIng. David Hudák
Jedná se o kvalitní práci s velkým průmyslovým potenciálem s mírnými nedostatky v technické zprávě vyváženými velmi silnou experimentální částí. Z toho důvodu doporučuji bakalářskou práci hodnotit známkou A.
Stupeň hodnocení: obtížnější zadání
Student se musel seznámit jak s tématem modelování a simulací v leteckém prostředí s pomocí nástroje MATLAB/Simulink, tak s teorií grafových izomorfismů v kontextu optimalizace efektivity testování, což není standardním obsahem bakalářského studia na naší fakultě. Hlavním zadáním práce pak bylo navrhnout a implementovat vhodnou heuristiku s využitím zmíněných grafových algoritmů pro nalezení optimální testovací strategie pro pokrytí všech unikátních testovacích scénářů. Implementované řešení bylo dle zadání nutné vyhodnotit na reálných průmyslových datech poskytnutých společností Honeywell. Z těchto důvodů hodnotím zadání jako mírně obtížnější.
Práce je členěna do 5 logických kapitol s tím, že dílčí texty jsou psány srozumitelně a vhodně se odkazují na přiložené ilustrace, ostatní sekce či případně naměřené výsledky. Potřebná teorie je vysvětlena srozumitelně s užitečnými příklady a experimentální fáze je popsána velmi detailně a čtivě. Méně srozumitelná mi přišla kapitola 3, která by dle mého názoru působila lépe, kdyby byla rozdělena například na kapitoly design a technical details, jelikož aktuálně kombinuje jak zásadní detaily teoretického návrhu, tak možná až zbytečně technické informace včetně vyčerpávajícího souhrnu jednotlivých implementovaných tříd a jejich funkcí/atributů.
Práce je po formální stránce vypracována velmi kvalitně. K samotnému textu mám tak pouze dvě drobné výhrady. První je nevyužití vektorové grafiky v případě Figure 3.1 a Figure 3.2, kdy obě ilustrace (alespoň v elektronické podobě), působí na první pohled rozmazaně. Druhou výtkou jsou občasné problémy se zarovnáním textu do bloku, např. v kapitole testování v případě Characteristics of Models. Úroveň angličtiny použité v práci je na kvalitní úrovni s občas mírně neobratnou strukturou vět, ale bez zásadních pravopisných chyb.
Realizačním výstupem je nástroj pro efektivní implementaci testů v prostředí modelů MATLAB/Simulink, který je rozsáhlým způsobem zdokumentován v samotné technické zprávě a následně aplikován na extenzivní sadu vhodně zvolených syntetických benchmarků i reálných úloh. Oceňuji přítomnost vlastní implementace tvorby syntetických pozitivních a negativních případů pro testovaní hledání izomorfismů. Mírná výtka směřuje k rozdělení do tří zcela separátních adresářů (částečně z licenčních důvodů) -- v rámci nějaké uživatelské přívětivosti mi chybí nějaká jasná centrální integrace uvedených nástrojů. Samotné zdrojové kódy jednotlivých nástrojů (v Pythonu a MATLABu) jsou ale jinak vhodně komentované, srozumitelné a nemám k nim žádných výtek.
S ohledem na to, že student využil implementovaný nástroj pro testování na reálných modelech poskytnutých společností Honeywell s velmi slibnými výsledky (redukce testovací sady kolem 50 % za 10 minut), lze očekávat vysokou využitelnost nástroje v praxi.
Stupeň hodnocení: zadání splněno
Výsledkem bakalářské práce je propojení tří nástrojů BLADE, BARLOG (tento nástroj částečně vznikl mimo bakalářskou práci) a BALIN vykazující významné zefektivnění testování s využitím snížení potřebných testovacích scénářů (modelů) na základě výpočtu grafových izomorfismů s pomocí algoritmu VF3. Implementaci se povedlo vyhodnotit na průmyslové modelové sadě poskytnuté společností Honeywell, čímž byly splněny všechny body zadání.
Stupeň hodnocení: je v obvyklém rozmezí
Vypracovaný text se nachází v požadovaném rozsahu pro bakalářskou práci. Text jako takový obsahuje vše podstatné.
Použitá literatura v bakalářské práci byla vhodně zvolena a pokrývá všechna témata diskutovaná ve vypracované práci. Jako určitou výtku bych uvedl zapracování některých referencí do textu práce, kdy některá tvrzení, která vychází z uvedené literatury, nejsou řádně ocitována -- např. v úvodu testování je tvrzení, že VF3 pracuje v čase O(n!*n), ale nikde v kapitole není uvedená reference na vysvětlení tohoto tvrzení. To samé platí i pro mnohé další definice či zmíněné praktické oblasti (např. bioinformatika v sekci State of the Art; 2.1). V některých sekcích či kapitolách (např. v celém Úvodu) pak citace zcela chybí.
Známka navržená oponentem: A
Odpovědnost: Mgr. et Mgr. Hana Odstrčilová