Přístupnostní navigace
E-application
Search Search Close
Master's Thesis
Author of thesis: Ing. Daniel Gavenda
Acad. year: 2023/2024
Supervisor: Ing. Jan Fiedor, Ph.D.
Reviewer: Ing. Aleš Smrčka, Ph.D.
Simulink diagrams are widely used in industry, where they are used to specify control systems. The specific block used in them is the Stateflow diagram. The specified systems are often critical from the point of view of security, therefore the question of the correctness of the implementation of these systems is important. In this work, we will focus on the design, description and creation of a tool for the reverse reconstruction of the Stateflow diagram from the optimized code in the C language in order to prove the functional equivalence between the model and its corresponding code. Next, a created set of models representing models with Stateflow diagrams and codes generated from them is created, using several optimizations. The created tool will be tested on this set, it can also be used to evaluate other Stateflow analyzes and/or C code.
Simulink, Stateflow, optimizations, translation validation, finite state automata, automatic code generation, reverse reconstruction, Honeywell
Date of defence
17.06.2024
Result of the defence
Defended (thesis was successfully defended)
Grading
B
Process of defence
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.
Topics for thesis defence
Language of thesis
Slovak
Faculty
Fakulta informačních technologií
Department
Department of Intelligent Systems
Study programme
Information Technology and Artificial Intelligence (MITAI)
Specialization
Machine Learning (NMAL)
Composition of Committee
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)
Supervisor’s reportIng. 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.
Grade proposed by supervisor: A
Reviewer’s reportIng. 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.
Evaluation level: zadání splněno
Evaluation level: 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.
Evaluation level: 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.
Grade proposed by reviewer: B
Responsibility: Mgr. et Mgr. Hana Odstrčilová