|
|
Vylepšení analýzy živých proměnných pomocí points-to analýzy
Raiskup, Pavel ; Rogalewicz, Adam (oponent) ; Dudka, Kamil (vedoucí práce)
Jazyky, jako je C, hojně využívají práce s ukazateli. Implemetace dynamických datových struktur vázaných ukazateli a operací nad nimi však není jednoduchá - významně zvyšuje rizika zanášení chyb do zdrojových kódů. Jedna z cest, jakými lze eliminovat množství těchto chyb, je použití statické analýzy. Tato práce se tedy zabývá vylepšením architektury Code Listner, která nabízí rozhraní pro tvorbu statických analyzátorů. Vlastností tohoto rozhraní je, že poskytuje takovému analyzátoru k rozboru potřebné informace o programu - ku příkladu databázi proměnných, graf toku řízení čí graf volání funkcí. Součástí implementace Code Listeneru je také algoritmus pro analýzu živých proměnných, umožňující odstranit, neboli zabít proměnné, které nejsou v daném místě grafu toku řízení potřeba. Původní algoritmus ale nedovedl z důvodu bezpečnosti zabít žádné proměnné, na něž byla kdekoliv ve zdrojovém kódu vzata adresa. Předpokládalo se, že taková proměnná může být zpřístupněna pomocí reference kdekoliv v programu. Cílem práce tedy bylo navrhnout a implementovat algoritmus pro points-to analýzu, která dovede vyloučit existenci některých referencí v daném kontextu programu a umožní tedy zefektivnit analýzu živých proměnných.
|
|
|
Statická analýza počítačových sítí
Hozza, Tomáš ; Veselý, Vladimír (oponent) ; Ryšavý, Ondřej (vedoucí práce)
Některé problémy v konfiguracích síťových zařízení jsou těžko identifikovatelné. Důležitou částí mnoha konfigurací jsou přístupové seznamy, ve kterých konflikty mezi pravidly mohou způsobit mezery v bezpečnostní politice nebo v kvalitě služeb. Tato práce je zaměřena právě na identifikaci a klasifikaci konfliktů mezi pravidly přístupového seznamu jednoho zařízení. Tento úkol není triviální, pokud chceme identifikovat všechny možné druhy konfliktů. V práci je uveden optimalizovaný algoritmus na kompletní analýzu přístupového seznamu s využitím binárních prefixových stromů, založený na existujícím výzkumu Baboescu a Varghese. S jeho použitím byl implementován nástroj schopný detekovat konflikty mezi pravidly přístupového seznamu zařízení Cisco, HP nebo Juniper. Kvůli menším paměťovým nárokům jsou bitové vektory v prefixových stromech komprimované WAH kompresní metodu. Implementovaný nástroj byl otestován s ohledem na správnost a výkonnost. Testy potvrdily potenciál použitého řešení výrazně urychlit analýzu přístupových seznamů.
|
|
|
Dynamická detekce a léčení časově závislých chyb nad daty v prostředí Java
Letko, Zdeněk ; Kolář, Dušan (oponent) ; Vojnar, Tomáš (vedoucí práce)
Hledání chyb plynoucích ze souběžného zpracovávání výpočtů je obtížné. Proto se tato diplomová práce zabývá detekcí a léčením časově závislých chyb nad daty a chyb plynoucích z nesprávné atomicity operací v prostředí Java. Práce prezentuje dva různé algoritmy pro detekci. Jedním z nich je nový algoritmus nazvaný AtomRace, který detekuje časově závislé chyby nad daty jako speciální případ nesprávné atomicity operací. Následné léčení detekovaných chyb je založeno na potlačení opakování chyby, buď zavedením přídavné synchronizace, nebo legálním ovlivňováním plánovače Javy, za účelem vynucení správné atomicity operací. Navržená architektura, která pracuje souběžně se sledovaným programem, využívá ke sledování a ovlivňování výpočtu techniku instrumentace na úrovni Java bytecode. Architektura a algoritmy byly implementovány a otestovány v několika případových studiích.
|
|
|
Verifikace ukazatelových programů pomocí lesních automatů
Hruška, Martin ; Rogalewicz, Adam (oponent) ; Holík, Lukáš (vedoucí práce)
V této práci je rozvíjena existující metoda pro shape analýzu programů založená na lesních automatech. Dále je také vylepšována implementace této metody, nástroj Forester. Lesní automaty jsou založeny na stromových automatech, jejichž jednoduchou implementaci Forester obsahuje. Prvním přínosem této práce je nahrazení této implementace knihovnou VATA, která obsahuje efektivní algoritmy pro reprezentaci a manipulaci stromových automatů. Verze nástroje Forester používající knihovnu VATA se zúčastnila mezinárodní soutěže SV-COMP 2015. Dále je verifikace založená na lesních automatech v této práci rozšířena o predikátovou abstrakci a analýzu nalezených protipříkladů. Výsledek této analýzy je možné využít následujícími způsoby. Prvním je určení toho, zda je nalezené chyba reálná nebo naopak nepravá. Druhým je pak zjemnění predikátové abstrakce pomocí predikátů odvozených při zpětném běhu. Obě techniky byly také implementovány v nástroji Forester. Na závěr je zhodnoceno zlepšení, které tyto techniky přinesly oproti původní verzi nástroje Forester.
|
|
|
Materiálově nelineární řešení konstrukcí z plastů
Weis, Lukáš ; Krejsa,, Martin (oponent) ; Králík,, Juraj (oponent) ; Kytýr, Jiří (oponent) ; Němec, Ivan (vedoucí práce)
Předkládaná práce se zaměřuje na statickou analýzu konstrukcí z plastů se zohledněním nelineárního chování materiálu v závislosti na napětí. Statická analýza je prováděna metodou konečných prvků. V úvodu práce je názorně popsán rozdíl mezi materiálově lineárním a materiálově nelineárním přístupem. Pro numerickou analýzu plastových konstrukcí je vhodné použít skořepinový konečný prvek rozšířený o možnost dalšího dělení na vrstvy a integrační body přes svoji výšku. Samostatné kapitoly se věnují integraci výsledných veličin přes výšku průřezu. Integrace materiálové matice tuhosti korektně zohledňuje vznik excentricity. Část pozornosti je věnována numerickým kvadraturním pravidlům. Následující kapitola se věnuje materiálově nelineárním modelům. Je popsán jednodušší přístup za pomoci izotropně nelineárně elastického modelu, dále je popsán obecný přístup za použití ortotropně plastického modelu. Teoretický popis je doplněn grafickou interpretací kritérií podle jednotlivých autorů. Významná část této práce je věnována algoritmizaci výpočetních postupů. Je provedena v jazyce Fortran do dynamicky linkované knihovny, která je součástí programu RFEM 5, který je široce využíván v technické praxi. Součástí práce je studie srovnávající výkonnost různých technologií použitelných pro algoritmizaci popisované problematiky. Správnost teoretické analýzy materiálových modelů a následné implementace do programu RFEM 5 je ověřena na příkladu ohýbané konzoly. Konstrukce termoplastové nadzemní nádrže je podrobena detailní materiálově lineární, resp. nelineární analýze. Různé přístupy jsou porovnány na výsledcích napětí, deformace a přetvoření. Zvláštní pozornost je pak věnována stabilitní analýze se zohledněním nelineárního materiálového modelu.
|
|
|
Vysokovýklopná lopata pro teleskopický manipulátor LM1345 TURBO
Dragan, Lukáš ; Kubín, Martin (oponent) ; Škopán, Miroslav (vedoucí práce)
Tato diplomová práce se zabývá řešením konstrukčního návrhu vysokovýklopné lopaty pro teleskopický manipulátor LM1345 TURBO firmy New Holland. Úvodem jsou zpracovány základní vlastnosti a parametry stroje a materiálu, k jehož přepravě bude lopata v provozu nejčastěji využita. Dále práce obsahuje statickou analýzu zatěžovacích stavů působících na lopatu a rám při provozu stroje, pevnostní výpočty a navržení a kontrolu použitých čepů.
|
|
|
Úprava držáku celohliníkového chladiče
Malovaný, Daniel ; Ramík, Pavel (oponent) ; Svída, David (vedoucí práce)
Cílem této diplomové práce je provést základní přehled konstrukčních řešení uchycení celohliníkových chladičů. Výpočtem pomocí metody konečných prvků provést kontrolu první generace držáku celohliníkového nízkoteplotního vodního chladiče a na základě tohoto výpočtu navrhnout úpravu jeho konstrukce, která povede ke snížení napětí v kritických oblastech. Na závěr toto nové řešení zhodnotit.
|
|
|
Vysokovýklopná lopata
Petro, Roman ; Lžičař, Roman (oponent) ; Škopán, Miroslav (vedoucí práce)
Tato diplomová práce řeší konstrukční návrh vysokovýklopné lopaty pro nakladače New Holand B100 a B110. Úvodem jsou pospány provozní podmínky, přepravovaný materiál a rypadlo-nakladač B100, B110. Jsou zde uvedena možná konstrukční řešení a vlastní konstrukční návrh. Následuje kinematický rozbor vykládání materiálu a statická analýza na lopatě a rámu. Na statickou analýzu navazuje kontrola čepů a pevnostní analýza lopaty i rámu pro různé zatěžovací stavy provedená metodou konečných prvků
|
|
| |
|
|
Analýza působení větru na stavební konstrukci
Tačner, Jan ; Hradil, Petr (oponent) ; Kala, Jiří (vedoucí práce)
Diplomová práce se zabývá statickou a dynamickou analýzou chování štíhlé mostní konstrukce. V programovém systému ANSYS 14.5 byl vytvořen výpočtový model konstrukce lávky. Byla provedena statická a modální analýza, na základě které bylo na konstrukci aplikováno náhradní dynamické zatížení od působení větru dle normy ČSN 73 0035, kde byla zohledněna varianta mostovky bez zábradlí či mostovky s plně neprodyšným zábradlím a dynamické zatížení vyvolané skupinou chodců a spojitým zástupem. Na tato zatížení byl proveden výpočet ustálené odezvy při rezonanci.
|
host ::
RSS.