Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
diplomová práce
Autor práce: Ing. Daniel Gavenda
Ak. rok: 2023/2024
Vedoucí: Ing. Jan Fiedor, Ph.D.
Oponent: Ing. Aleš Smrčka, Ph.D.
Simulink diagramy majú široké využitie v priemysle, kde sa používajú na špecifikáciu riadiacich systémov. Konkrétnym blokom, ktorý sa v nich používa je Stateflow (stavový) diagram. Špecifikované systémy sú často kritické z hľadiska bezpečnosti, preto je otázka správnosti implementácie týchto systémov dôležitá. V tejto práci sa zameriame na návrh, popis a vytvorenie nástroja na spätnú rekonštrukciu Stateflow diagramu z optimalizovaného kódu v jazyku C za účelom preukázania funkčnej ekvivalencie medzi modelom a jemu odpovedajúcim kódom. Ďalej je vytvorená sada modelov reprezentujúcich modely so Stateflow diagramami a z nich vygenerované kódy pomocou viacerých optimalizácií. Na tejto sade bude vytvorený nástroj otestovaný, tiež je možné túto využiť pre evaluáciu iných analýz Stateflow a/alebo C kódu.
Simulink, Stateflow, optimalizácie, validácia prekladu, konečné stavové automaty, automatické generovanie kódu, spätná rekonštrukcia, Honeywell
Termín obhajoby
17.06.2024
Výsledek obhajoby
obhájeno (práce byla úspěšně obhájena)
Klasifikace
B
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 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 k obhajobě
Jazyk práce
slovenština
Fakulta
Fakulta informačních technologií
Ústav
Ústav inteligentních systémů
Studijní program
Informační technologie a umělá inteligence (MITAI)
Specializace
Strojové učení (NMAL)
Složení komise
prof. Dr. Ing. Jan Černocký (předseda) doc. Ing. Lukáš Burget, Ph.D. (člen) doc. Mgr. Lukáš Holík, Ph.D. (člen) doc. RNDr. Pavel Smrž, Ph.D. (člen) doc. Ing. Vítězslav Beran, Ph.D. (člen) Ing. František Grézl, Ph.D. (člen)
Posudek vedoucíhoIng. Jan Fiedor, Ph.D.
Celkově hodnotím práci velmi kladně. Student se vypořádal s obtížným zadáním nadmíru dobře, navíc nad rámec požadavků zadání implementoval transformaci Stateflow diagramu do stejné reprezentace jako při zpětné rekonstrukci z kódu a jednoduchou metodu pro ověřování ekvivalence těchto reprezentací. Kromě toho také připravil věřejnou sadu Stateflow modelů s mnoha variantami různě optimalizovaného kódu generovaného z těchto modelů, jenž lze využít s výhodou nejen pro evaluaci této práce ale i pro další výzkumné účely.
Cílem práce bylo navrhnout metodu pro zpětnou rekonstrukci Stateflow diagramu nástroje MATLAB Simulink z kódu v jazyce C, který generuje překladač MATLAB Embeded Coder právě z tohoto typu digramu. Cílem zpětné rekonstrukce je vytvořit interní reprezentaci Stateflow diagramu vhodnou pro ověřování ekvivalence.
Kromě návrhnu interní reprezentace a metody pro zpětnou rekonstrukci kódu implementoval student také transformaci Stateflow diagramu do navržené interní reprezentace a jednoduchou metodu pro ověřování ekvivalence interních reprezentací původního Stateflow diagramu a jeho verze zpětně zrekonstruované z kódu. Zadání tedy hodnotím jako obtížnější.
Práce byla vytvořena ve spolupráci se společností Honeywell, kde je nástroj již částečně integrován do interního nástroje pro ověřování funkční ekvivalence mezi modelem a kódem pro účely certifikace.
Technická zpráva byla konzultována s vedoucím i technickým vedoucím behěm posledních dvou týdnů před odevzdáním. Student zapracoval několik iterací připomínek, i když jedna či dvě další iterace by technické zprávě prospěly. Zpráva ale obsahuje všechny důležité informace pro pochopení cílů a výsledků práce.
Experimentální verze práce je již integrována do interního nástroje firmy Honeywell pro ověřování ekvivalence modelů a kódu pro účely certifikace, kde pomůže eliminovat potřebu manuálního peer review pro kód generovaný ze Stateflow modelů. Finální verze práce se aktuálně připravuje k integraci. Honeywell i technický vedoucí z firmy Honeywell jsou výsledky práce velmi potěšeni a plánují nadále se studentem spolupracovat na vývoji tohoto nástroje.
Student využil zdroje informací doporučených vedoucími práce i sám aktivně vyhledával relevantní zdroje informací k řešení diplomové práce. Díky úzkému zaměření práce na oblast certifikace avionických komponent tato práce využívá velmi specifické zdroje informací jako jsou značně rozsáhlé standardy pro oblast avioniky.
Student byl velmi aktivní během celého řešení práce, návrh i implementaci průběžně konzultoval s technickým vedoucím práce ze společnosti Honeywell, kdy byl vždy připraven a aktivně přicházel s vlastnímy myšlenkami řešení dané problematiky.
Známka navržená vedoucím: A
Posudek oponentaIng. Aleš Smrčka, Ph.D.
Studen dosáhl dobrého a hlavně v praxi použitelného výsledku a technická zpráva je na velmi dobré úrovni.
Stupeň hodnocení: zadání splněno
Stupeň hodnocení: je v obvyklém rozmezí
Technická zpráva má cca 80 normostran textu včetně obrázků.
Technická zpráva obsahuje všechny hlavní části. Analýza dané problematiky a popis nástroje Simulink i jeho dopad na generování kódu jsou obsahově podrobné. Oceňuji bližší prozkoumání důsledků různých optimalizací kódu nástrojem Simulink. Popis vlastní implementace by si zasloužil více detailů s vazbou na zdrojové kódy nebo stuktur v nich použitých. Diplomová práce se zabývá modely zdrojových kódů, a proto by se hodilo využít některé ze standardních diagramů (SysML či UML) i pro popis vlastního přínosu.
Formální úprava je na dobré úrovni. Má však některé nedostatky:
Technická zpráva by si zasloužila ještě jeden kontrolní průchod. Obsahuje ojedinělé významové chyby, např. poslední věta druhého odstavce na str. 14 nedává smysl nebo, na stejné stránce, je chyba v posledním řádku: místo "out32 <= 5" má být "in32 <= 5".
Použitá literatura je skromná, ale s ohledem na téma práce je výběr v pořádku. Zahrnuje odkazy na standardy související s návrhem a vývojem systémů, použité nástroje a 2 odborné knihy. Autor mohl citovat více zdrojů z oblasti atuomatického generování nebo analýzy zdrojových kódů.
Technické řešení zahrnuje program v jazyce Java. Řešení mi bylo demonstrováno a je funkční. Zdrojové kódy mají více než 9 tis. řádků kódu a mají logickou strukturu. Nedostatkem je chybějící licence a velmi skromné komentáře (zdrojovým kódům chybí hlavička s autorem).
Menší nedostatek: Nástroj se nepovedlo zprovoznit v kontejneru posledního vydání Maven (s Java ver. 21) založeném na distribuci Ubuntu. Řešení však bylo úspěšně demonstrováno na MS Windows.
Výsledný nástroj má jasné použití v praxi, kde na něj lze navázat při ověřování ekvivalence mezi modely řídicích systémů a jejich zdrojovými kódy generovanými z nich.
Stupeň hodnocení: obtížnější zadání
Práce zahrnuje spojení oblastí generování zdrojových kódů z modelů systému a statické analýzy zdrojových kódů. Ke splnění cíle bylo potřeba se podrobně seznámit s nástrojem Mathlab Simulink a jeho možnostmi při generování zdrojových kódů, se Stateflow diagramy použitými při vývoji reálných řídicích zařízeních a navržení a implementace nástroje pro zpětné získání modelu v podobě stavových diagramů umožňující jejich porovnání s původním modelem systému.
Známka navržená oponentem: B
Odpovědnost: Mgr. et Mgr. Hana Odstrčilová