|
|
Jeřáb mostový
Plášil, František ; Malach, František (oponent) ; Malášek, Jiří (vedoucí práce)
Práce se zabývá konstrukčním návrhem mostového jeřábu. V první části je provedena rešerše a popis jednotlivých částí jeřábu. Tu následuje volba vhodné koncepce s ohledem na zadané parametry diplomové práce. Je navrhnuta nosná konstrukce jeřábu, která je doplněna důležitými pevnostními a technickými výpočty. Ty jsou provedeny dle platných státních norem. V závěrečné části je proveden výpočet konstrukce pomocí metody konečných prvků a navrhnuta finanční rozvaha projektu. K práci je přiložena výkresová dokumentace obsahující sestavný výkres jeřábu a vybrané detailní výkresy.
|
|
|
Ochrana zdraví uživatele 3D tiskárny
Plášil, František ; Kočiš, Petr (oponent) ; Halamíček, Lukáš (vedoucí práce)
Tato bakalářská práce se zabývá ochranou zdraví uživatele 3D tiskárny. V první části je pojednáno o současném stavu poznání, který uvádí technologie 3D tisku využívaných v současné době a následně rozbor technologie Fused deposition modeling. Dále je uvedena problematika této technologie, a na závěr je navrhnuto konkrétní opatření k předejití zdravotních rizik, s touto technologií spojených.
|
|
|
Jeřáb mostový
Plášil, František ; Malach, František (oponent) ; Malášek, Jiří (vedoucí práce)
Práce se zabývá konstrukčním návrhem mostového jeřábu. V první části je provedena rešerše a popis jednotlivých částí jeřábu. Tu následuje volba vhodné koncepce s ohledem na zadané parametry diplomové práce. Je navrhnuta nosná konstrukce jeřábu, která je doplněna důležitými pevnostními a technickými výpočty. Ty jsou provedeny dle platných státních norem. V závěrečné části je proveden výpočet konstrukce pomocí metody konečných prvků a navrhnuta finanční rozvaha projektu. K práci je přiložena výkresová dokumentace obsahující sestavný výkres jeřábu a vybrané detailní výkresy.
|
|
|
Formal Verfication of Components in Java
Parízek, Pavel ; Plášil, František (vedoucí práce) ; Černá, Ivana (oponent) ; Pasareanu, Corina (oponent)
Formal veri cation of a hierarchical component application involves (i) checking of behavior compliance among sub-components of each composite component, and (ii) checking of implementation of each primitive component against its behavior speci cation and other properties like absence of concurrency errors. In this thesis, we focus on veri cation of primitive components implemented in Java against the properties of obeying a behavior speci cation de ned in behavior protocols (frame protocol) and absence of concurrency errors. We use the Java PathFinder model checker as a core veri cation tool. We propose a set of techniques that address the key issues of formal veri cation of real-life components in Java via model checking: support for high-level property of obeying a behavior speci cation, environment modeling and construction, and state explosion. The techniques include (1) an extension to Java PathFinder that allows checking of Java code against a frame protocol, (2) automated generation of component environment from a model in the form of a behavior protocol, (3) efficient construction of the model of environment's behavior, and (4) addressing state explosion in discovery of concurrency errors via reduction of the level of parallelism in a component environment on the basis of static analysis of Java...
|
|
|
Behavior Protocols Extensions
Kofroň, Jan ; Plášil, František (vedoucí práce) ; Richta, Karel (oponent) ; Assmann, Uwe (oponent)
Formal verification of behavior of a component application requires a suitable specification language. It is necessary that the specification language captures all important aspects of the future implementation with respect to desired properties. Behavior Protocols have been proven to be a suitable component behavior specification platform if one is interested in absence of communication errors. In this thesis, we (1) propose a new specification language based on Behavior Protocols and (2) address the issue of insufficient performance of BPChecker-a proprietary tool for verification of absence of communication errors in Behavior Protocols. Motivated by issues raised during specification of a real-life-sized case study aiming at providing wireless Internet access at airports, we extended the original Behavior Protocols with support for method parameters, local variables, synchronization of more than two components, and specification of variable-controlled loops. To address the second issue, we propose a method for verification of Behavior Protocols via their transformation to Promela-the input language of the Spin model checker.
|
|
|
Automated verification of software
Šerý, Ondřej ; Plášil, František (vedoucí práce) ; Janeček, Jan (oponent) ; Ghezzi, Carlo (oponent)
Přes výzkumné usilí věnované automatické veri kaci software, její pronikání do softwarového průmyslu je stále spíše pomalé. Toto váhání mělo několik důvodů 1) složitost posouzení jednotlivých nástrojů, 2) složitost použití nástrojů a jejich integrace do vvývojového procesu. Pro usnadnění výběru jednotlivých nástrojů je součástí práce přehled technik založených na model checkingu kódu s porovnáním technik na základě jednotných kritérií. Navíc práce obsahuje průmyslovou případovou studii používající model checker BLAST. K posouzení vhodnosti nástrojů je potřeba i odpovovídajícího vzdělání, přikládáme tedy i své zkušenosti s přípravou dvou magisterských přednášek o formálních metodách. Integrací snadno použitelného speci kačního jazyka do model checkeru BLAST, přispíváme k usnadnění použití tohoto nástroje. Mimo to představujeme koncept unit checkingu, tedy kombinace unit testingu a model checkingu kódu. Unit checking pomáhá s integrací model checkingu kódu do vývojového procesu.
|
|
|
Towards thread aware component behavior specifications
Poch, Tomáš ; Plášil, František (vedoucí práce) ; Černá, Ivana (oponent) ; Hennicker, Rolf (oponent)
Komponentový přístup je již poměrně zavedenou metodologií používanou při vývoji software. Při komerčním vývoji aplikací, se však ještě nevyužívají modely chování komponent a jejich následná analýza, ačkoliv by to zaručilo, že komunikace mezi složenými komponentami nebude obsahovat chyby. Reálnému použití v praxi brání jkk relativně omezené výrazové prostředky modelovacích jazyků tak i náročnost psaní modelů. Abychom usnadnili použití modelů chování, navrhujeme modelovací jazyk Threaded Behavior Protocols (TBP), který se snaží překlenout rozdíly mezi modelovacími a imperativními programovacími jazyky. Tím, že umožníme programátorům používat koncepty z imperativních jazyků, na které jsou zvyklí, usnadníme přípravu modelů. Teorie TBP de finuje pojem správnosti kompozice komponent jako absenci dvou pevně daných komunikačních chyb a poskytuje relaci zjemňovíní modelu, která zachovává správnost vzhledem k libovolnému prostředí. Díky tomu, přináší analýza TBP podobné výhody jako starší modelovací jazyky, přičemž bere v úvahu i koncepty z imperativních jazyků.
|
|
|
Towards Static Analysis of Languages with Dynamic Features
Hauzar, David ; Plášil, František (vedoucí práce) ; Sinz, Carsten (oponent) ; Holík, Lukáš (oponent)
Dynamické funkce programovacích jazyků, jako je dynamický typový systém, dynamické volání funkcí, dynamické vykonávání kódu a dynamické datové struktury, poskytují flexibilitu, která urychluje vývoj. Tyto funkce ale snižují množství informací, které jsou kontrolovány v době kompilace. To má za následek nižší výkon a větší chybovost programů. Tento problém je možné vyřešit pomocí technik statické analýzy. Dynamické funkce bohužel pro tyto techniky představují překážku a zásadně omezují jejich přesnost, spolehlivost a výkonnost. Abychom tento problém pomohli vyřešit, navrhujeme framework pro statickou analýzu, který automaticky řeší dynamické funkce, a tím umožňuje definovat přesné a spolehlivé statické analýzy podobně jako v případě, kdy program dynamické funkce neobsahuje. Aby bylo takový framework možné vytvořit, navrhujeme novou techniku heap analýzy, která modeluje asociativní pole a (prototypové) objekty. Dále navrhujeme analýzu hodnot proměnných, která zjišťuje další informace potřebné pro vypořádání se s dynamickými funkcemi. Nakonec navrhujeme techniku, která umožňuje automaticky a genericky kombinovat analýzu hodnot proměnných s heap analýzou. Powered by TCPDF (www.tcpdf.org)
|
|
|
Hierarchical Component Models - "A True Story"
Ježek, Pavel ; Plášil, František (vedoucí práce) ; Brada, Přemysl (oponent) ; Crnkovic, Ivica (oponent)
Práce se nejprve zabývá analýzou širokého spektra konceptů a přístupů ke komponentově orientovanému návrhu software a předkládá přehled vybraných komponentových modelů s běhovým prostředím strukturovaný podle nově navržených kritérií. Hierarchické komponentové modely jsou identifikovány jako jeden z přístupů, který ještě není dostatečně prozkoumán, vzhledem k jejich minimálnímu proniknutí do světa průmyslových aplikací. Zbytek práce se pak téměř výhradně věnuje problémům spojeným s nasazením hierarchických komponentových modelů v reálném vývoji softwarových aplikací. Práce představuje motivace vedoucí k nutnosti hierarchického strukturování aplikačních architektur a dále na příkladech z komerční sféry uvádí hlavní výhody vývoje aplikací pomocí hierarchických komponentových modelů. Jako důkaz jsou předvedeny dvě případové studie, které jsou úspěšně vymodelované a implementované pro komponentový model Fractal - práce se zaměřuje hlavně na formální ověřitelnost správnosti takto vytvořených aplikací. Na základě zkušeností z případových studií jsou v práci též předloženy návrhy nového přístupu pro modelování dynamických architektur, identifikování chyb v chybových výstupech a specifikační jazyk pro modelování okolí komponent.
|
|
|
Ochrana zdraví uživatele 3D tiskárny
Plášil, František ; Kočiš, Petr (oponent) ; Halamíček, Lukáš (vedoucí práce)
Tato bakalářská práce se zabývá ochranou zdraví uživatele 3D tiskárny. V první části je pojednáno o současném stavu poznání, který uvádí technologie 3D tisku využívaných v současné době a následně rozbor technologie Fused deposition modeling. Dále je uvedena problematika této technologie, a na závěr je navrhnuto konkrétní opatření k předejití zdravotních rizik, s touto technologií spojených.
|
host ::
RSS.