|
|
Improving Precision of Program Analysis in the 2LS Framework
Smutný, Martin ; Vojnar, Tomáš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this work is to propose a way to improve precision of program analysis in the 2LS framework, based on its existing concepts, mainly template-based synthesis of invariants. 2LS is a static analysis framework for analysing C programs which relies on the use of an SMT solver and of abstract interpretation for automatic invariant inference. In a case when 2LS can not decide whether a program is correct, the proposed solution analyses the invariants computed in various abstract domains and identifies parts of the invariants that potentially cause undecidability of the verification. Using the obtained information, the designed method is able to identify variables of the original program that possibly determine whether the verification is successful. The output of our solution can be used as a feedback to indicate variables with problematic values that should be constrained. Also, it can be utilized by the 2LS developers for debugging purposes during development of new analyses. The solution has been implemented in the 2LS framework. Testing our solution on various benchmarks from the International Competition on Software Verification (SV-COMP) shows that it can identify variables that cause undecidability of the verification in more than half of the programs where the verification currently fails.
|
|
|
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ů.
|
|
|
Network-wide Security Analysis
de Silva, Hidda Marakkala Gayan Ruchika ; Šafařík,, Jiří (oponent) ; Šlapal, Josef (oponent) ; Švéda, Miroslav (vedoucí práce)
The objective of the research is to model and analyze the effects of dynamic routing protocols. The thesis addresses the analysis of service reachability, configurations, routing and security filters on dynamic networks in the event of device or link failures. The research contains two main sections, namely, modeling and analysis. First section consists of modeling of network topology, protocol behaviors, device configurations and filters. In the modeling, graph algorithms, routing redistribution theory, relational algebra and temporal logics were used. For the analysis of reachability, a modified topology table was introduced. This is a unique centralized table for a given network and invariant for network states. For the analysis of configurations, a constraint-based analysis was developed by using XSD Prolog. Routing and redistribution were analyzed by using routing information bases and for analyzing the filtering rules, a SAT-based decision procedure was incorporated. A part of the analysis was integrated to a simulation tool at OMNeT++ environment. There are several innovations introduced in this thesis. Filtering network graph, modified topology table, general state to reduce the state space, modeling devices as filtering nodes and constraint-based analysis are the key innovations. Abstract network graph, forwarding device model and redistribution with routing information are extensions of the existing research. Finally, it can be concluded that this thesis discusses novel approaches, modeling methods and analysis techniques in the area of dynamic networks. Integration of these methods into a simulation tool will be a very demanding product for the network designers and the administrators.
|
|
|
Statické a dynamické posouzení konstrukce vyhlídkové věže
Valíček, Jan ; Kala, Jiří (oponent) ; Salajka, Vlastislav (vedoucí práce)
Tato práce se zabývá statickou a dynamickou analýzou vyhlídkové věže. Jedná se o dřevěnou rozhledu v obci Bohdaneč. Pro dynamickou analýzu byl vytvořen podrobný výpočtový model v programu ANSYS. Statická analýza byla provedena v programu Scia Engineer. Oba programy využívají metodu konečných prvků. Pozornost byla věnována zatížení větrem dle Eurokódu 1, zatížení námrazou, výpočtu dynamického součinitele a odezvě na odtrhávání vírů. Práce obsahuje také posouzení vybraných částí konstrukce dle Eurokódů.
|
|
|
Statická analýza pružně podepřených konstrukcí
Šnajdárková, Jana ; Brdečko, Luděk (oponent) ; Vlk, Zbyněk (vedoucí práce)
Práce se zaměřuje na porovnání statických výpočtů na různých typech modelů. Ty jsou vypočítány jak ručními výpočty, tak v programu RFEM. Bez použití softwaru jsou vytvořeny zjednodušené prutové modely na pevných a pružných podporách a na nich jsou vypočítány podporové reakce, posouvající síly a ohybové momenty. Jedna část se zaměřuje na výpočet redukce ohybových momentů k docílení přesnějších výsledků. Pomocí programu jsou vytvořeny jak modely prutové tak prostorové, které jsou složeny z ploch. Dále je vytvořen model s prutem rozděleným a podepřeným tak, aby vznikla redukce ohybových momentů nad podporami. Posledním modelem je nosník se dvěma oddělenými komorami, které jsou vetknuty do desky a definovány jako žebra která s deskou spolupůsobí. Vnitřní sily na všech modelech se následně porovnávají.
|
|
| |
|
|
Analýza odezvy výškové uskladňovací nádrže na statické a dynamické zatížení
Strnadlová, Kateřina ; Vlk, Zbyněk (oponent) ; Nevařil, Aleš (vedoucí práce)
Tato bakalářská práce se zabývá návrhem a posouzením konstrukce vodojemu na statická a dynamická zatížení. V úvodu jsou popsány základní konstrukční typy vodojemů, jejich statické řešení a podmínky návrhu. Je proveden předběžný výpočet pro stanovení tloušťky skořepinové konstrukce a navržená konstrukce je poté řešena pomocí metody konečných prvků (MKP) v systému ANSYS. Na závěr je provedeno ověření únosnosti, stability a použitelnosti dle odpovídajících norem ČSN EN.
|
|
|
Nástroj pro hodnocení úhlednosti zdrojových souborů
Jahoda, David ; Smrčka, Aleš (oponent) ; Veigend, Petr (vedoucí práce)
Tato práce se zabývá tvorbou nástroje, jenž by umožňoval kontrolu a hodnocení úhlednosti zdrojových kódů v jazyce C. Primární cílovou skupinou jsou studenti předmětu Základy programování. Způsob realizace uvažuje využití nástroje Clang-Tidy, rozšířeného o vlastní sadu kontrol a programu vyhodnocující výsledky kontrol na základě vstupní konfigurace. Vytvořený program je schopen bodově hodnotit zdrojové kódy za pomoci 16 kontrol dle konfigurace. Tyto kontroly odhalují různé začátečnické chyby. Z testování studentských projektů vyplynulo, že nejčastější chybou je využívání tzv. magických čísel. Program je možno s vhodným poučením studentů nasadit v předmětu Základy programování (IZP).
|
|
|
Statická a dynamická analýzy ocelové konstrukce
Uherek, Jan ; Martinásek, Josef (oponent) ; Vlk, Zbyněk (vedoucí práce)
Tato diplomová práce se zabývá popisem a statickou a dynamickou analýzou stávající vyhlídkové konstrukce. Jedná se o ocelovou rozhlednu v obci Město Albrechtice, kterou tvoří dvě příhradové věže spojené lávkou. Pro dynamickou i statickou analýzu byly vytvořeny podrobné výpočtové modely v programu SCIA Engineer 19.1, který pracuje na principu metody konečných prvků. Pozornost byla věnována zatížení větrem podle Eurokódu 1 a Eurokódu 3, zatížení námrazou, výpočtu dynamického součinitele. Práce obsahuje také posouzení vybraných částí konstrukce podle Eurokódů.
|
|
|
Statická analýza lávky pro pěší
Holada, Jiří ; Kala, Jiří (oponent) ; Hradil, Petr (vedoucí práce)
Práce se zabývá statickou analýzou a sestavením výpočtového modelu visutého mostu pro pěší a cyklisty přes řeku Sázavu v obci Zbořený Kostelec. Model je vytvořen podle skutečné podoby stavby. Délka lávky je 135 m a šířka 4 m. Výpočet sestavení výpočtového modelu je provedeno v programu ANSYS free Student Software.
|
host ::
RSS.