|
|
Improving Precision of Program Analysis in the 2LS Framework
Smutný, Martin ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Cílem této práce je navrhnout způsob vedoucí ke zvýšení přesnosti analýzy programů pomocí nástroje 2LS, založený na existujících konceptech, a to hlavně na syntézi invariant na základě šablon. 2LS je nástroj pro statickou analýzu programů napsaných v jazyce C, který využívá SMT solver a abstraktní interpretaci k automatickému odvození invariant. V případě kdy 2LS nedokáže rozhodnout zda je program správný, navrhované řešení analyzuje invarianty vypočítané v různých abstraktních doménách, a identifikuje takové části invariant, které mohou s největší pravděpodobností způsobit nejednoznačnost verifikace. Pomocí těchto získaných informací, dokáže navrhnutá metoda identifikovat proměnné původního programu, na kterých pravděpodobně závisí úspěch verifikace. Výstup tohoto řešení může posloužit jako zpětná vazba indikující proměnné, jejíchž problematické hodnoty by měly být omezeny. Také může být výstup využit vývojáři 2LS pro účely debugování při vývoji nových analýz. Řešení bylo implementováno v nástroji 2LS. Na základě různých experimentů mezinárodní soutěže ve verifikaci programů SV-COMP, dokáže řešení identifikovat proměnné způsobující nejednoznačnost verifikace ve více než polovině programů, na kterých verifikace momentálně selhává.
|
|
|
High loading shovel for telehandlers LM1345 Turbo
Dragan, Lukáš ; Kubín, Martin (referee) ; Škopán, Miroslav (advisor)
This diploma thesis follow up the structural design high loading shovel for telehandlers LM1345 TURBO by New Holland. The introduction processed basic characteristics and parameters of the machine and material which will be in operation most frequently transported by the shovel. The work includes static analysis load acting on the shovel and frame when the machine is operating, strength calculations and the design and control of the peg.
|
|
|
Network-wide Security Analysis
de Silva, Hidda Marakkala Gayan Ruchika ; Šafařík,, Jiří (referee) ; Šlapal, Josef (referee) ; Švéda, Miroslav (advisor)
Práce představuje model a metody analýzy vlasností komunikace v počítačových sítích. Model dosažitelnosti koncových prvků v IP sítích je vytvořen na základě konfigurace a síťové topologie a umožňuje ukázat, že vabraný koncový uzel je dosažitelný v dané síťové konfiguraci a stavu. Prezentovaná práce se skládá ze dvou částí. První část se věnuje modelování sítí, chování směrovaích protokolů a síťové konfiguraci. V rámci modelu sítě byla vytvořena modifikovaná topologická tabulka (MTT), která slouží pro agregaci síťových stavů určených pro následnou analýzu. Pro analýzu byl použit přístup založený na logickém programování, kdy model sítě je převeden do Datalog popisu a vlastnosti jsou ověřovány kladením dotazů nad logickou databází. Přínosy práce spočívají v definici grafu síťových filtrů, modifikované topologické tabulce, redukce stavového prostoru agrgací síťových stavů, modelů aktivního síťového prvku jako filter-transformace komponenty a metoda pro analýzu dosažitelnosti založena na logickém programování a databázích.
|
|
|
Static and dynamic assessment of an outlook tower construction
Valíček, Jan ; Kala, Jiří (referee) ; Salajka, Vlastislav (advisor)
This thesis deals with static and dynamic analysis of an lookout tower construction. For dynamic analysis a computational model in ANSYS software is created. Static analysis is performed by Scia Engineer software. Both of this software use finite element method. It is also focused on wind load determination by Eurocode 1, structural factor calculation, modal analysis and vortex shedding. Verification of selected parts according to Eurocodes is included.
|
|
|
Static analysis of flexibly supported on structures
Šnajdárková, Jana ; Brdečko, Luděk (referee) ; Vlk, Zbyněk (advisor)
This work focuses on comparing the static analysis on the various types of models. It is calculated as manual calculations and in software RFEM. Without use of the software are created simplified beam model on fixed and flexible supports and to them are calculated support reactions, shear forces and bending moments. One part focuses on the calculation of the reduction of bending moments, to achieve more accurate results. In the program are created models of rod and models of space, which are composed of surfaces. There is also created a model of the split rod to form a reduction of the bending moments over the supports. The last model is a beam with two separate chambers, which are fixed to the plate and defined as ribs which cooperates with the plate. Internal forces on all models is then compared.
|
|
| |
|
|
Response analysis of high-rise storage tank to static and dynamic loads
Strnadlová, Kateřina ; Vlk, Zbyněk (referee) ; Nevařil, Aleš (advisor)
This thesis describes the design and construction of water reservoir assessment for static and dynamic loads. The intoduction describes the basic design type sof reservoirs, thein static solution and design conditions. It made a preliminary calculation for determining the thickness of the shell structure and designed structure is then solid using the finite element metod (FEM) in ANSYS. In conclusion, verification of load-carrying capacity, stability and usability according to standard ČSN EN.
|
|
|
The Tool for Assessing the Neatness of Source Code
Jahoda, David ; Smrčka, Aleš (referee) ; Veigend, Petr (advisor)
This work deals with creation of tool that would allow the checking and evaluation of neatness of source codes in the C language. The primary user group are students of Introduction to Programming Systems (IZP). The implementation considers the use of Clang-Tidy tool (extended with custom set of checks) and program that evaluates results of checks based on the input configuration. The created program is capable of scoring source code using 16 checks according to the configuration. These checks detect various beginners errors. Testing of the student projects revealed that the most common error is the use of so-called magic numbers. The program can be deployed in the Introduction to Programming Systems (IZP) course with appropriate student instruction.
|
|
|
Static and dynamic analysis of steel structure
Uherek, Jan ; Martinásek, Josef (referee) ; Vlk, Zbyněk (advisor)
The thesis deals with a description and a static and dynamic analysis for an existing construction of lookout tower. The steel watchtower is located in Město Albrechtice and is made up of two lattice towers connected by a bridge. Main point was to create calculation models for the purpose of dynamic and static analysis, in the software SCIA Engineer 19.1, which is based on the principle of finite element method. Attention was paid to load created by winds according to Eurocode 1 and Eurocode 3, glaze and rime ice load and dynamic coefficient calculation. The thesis also includes an assesment of selected parts of the construction according to Eurocodes.
|
|
|
Static analysis of pedestrian bridge stucture
Holada, Jiří ; Kala, Jiří (referee) ; Hradil, Petr (advisor)
The thesis is focused on a static analysis and compiling a computational model of the suspension bridge for pedestrians and cyclists over the Sázavu river in Zbořený Kostelec vilage. The model is constructed according to the real shape of the structure. The length of the footbridge is 135 m and width 4 m. The calculation and compiling a computational model is processed by program ANSYS free Student Software.
|
guest ::
