|
|
Vektorový editor se zaměřením na animace
Kruliš, Martin ; Zavoral, Filip (vedoucí práce) ; Parízek, Pavel (oponent)
Předmětem této práce je implementace vektorového editoru s podporou animací. Program je určen pro specifickou oblast uživatelů, kteří potřebují vytvářet jednoduché animace a je pro ně zbytečné pořizovat komplexní komerční nástroje. V aplikaci bude možné navrhovat základní vektorové objekty, editovat je a nechat jejich body pohybovat po křivkách. Aplikace se vyznačuje především svou modularitou a flexibilitou, které umožní její snadné budoucí rozšiřování a přizpůsobení požadavkům uživatele.
|
|
|
Checking Primitive Component Behavior
Klika, David ; Kofroň, Jan (vedoucí práce) ; Parízek, Pavel (oponent)
Software model checking je metoda ověřování vlastností programů a tedy zajišťování jejich vyšší spolehlivosti. Je však stále nutné dělit programy na části ověřované nezávisle, Nebot' úplné programy tvoří často příliš velký stavový prostor, který není možné prozkoumat v rozumném čase. Softwarové komponenty dělí aplikace na čáasti vhodným způsobem. Ale vzhledem k tomu, jak fungují model checkery, je nutné jim poskytnout vhodné prostředí pro ověření každé komponenty. Pro popis chování komponent vznikly behavior protokoly. Umožňují ověřovat kompatibilitu a shodu chování komponent - to se používá již při návrhu aplikací pro odhalení možných nevhodných použití komponent. Protokoly jsou také vhodné jako popis chování komponenty, který může být srovnán s chováním konkrétní implementace komponenty. Cílem této pr¶ace je poskytnout nástroj pro srovnání chování primitivní komponenty oproti její specifikaci. V rámci toho bude implementován generátor prostředí komponent podle frame protokolu, které umožní rozpoznat porušení specifikace chování. Bude použit Java PathFinder a Fractal component model.
|
|
| |
|
|
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...
|
|
|
Preprocesor Java bytecode pro verifikační nástroje
Šafařík, Tomáš ; Parízek, Pavel (vedoucí práce) ; Hnětynka, Petr (oponent)
Nástroje J2BP a PANDA umožňují verifikovat zkompilované Java programy. V současné době tyto nástroje nejsou schopny správně zpracovat programy s určitými sekvencemi instrukcí JVM bytecodu. Tyto sekvence instrukcí jsme popsali a navrhli jejich transformace. Na základě těchto návrhů jsme implementovali novou aplikaci BytecodeTransformer. Tato aplikace transformuje zkompilované Java programy a nahrazuje v nich problematické sekvence instrukcí bytecodu. Díky tomu se tedy rozšířila množina programů, které nástroje J2BP a PANDA dokážou verifikovat. Dále jsme vyhodnotili aplikaci BytecodeTransformer prostřednictvím našich i cizích Java programů. Tyto testy ukázaly správnou funkcionalitu implementované aplikace. Powered by TCPDF (www.tcpdf.org)
|
|
|
Source Code Similarity Detection
Lano, Radek ; Tůma, Petr (vedoucí práce) ; Parízek, Pavel (oponent)
Cílem této diplomové práce je návrh a vývoj nástroje použitelného pro detekci podobných zdrojových kódů v různých projektech. Nástroj by měl být schopný nalézt kód zkopírovaný z jednoho projektu do druhého a měl by si poradit s běžnými pokusy o zmaření nalezení, jakými je například přejmenování symbolů, změna na sobě nezávislých entit, přesunutí entit do jiných souborů, přidání či odebrání komentářů, apod. Nástroj je implementován v jazyce C++ a připraven pro porovnávání zdrojových kódů v jazycích C a C++. Nástroj umožňuje i porovnávání zdrojových kódů v jiných jazycích, které je možné překládat pomocí kompilátoru GNU C Compiler. Pro kvalitní použití nástroje na takové zdrojové kódy je však potřeba připravit přídavné moduly (to je dáno odlišnou vnitřní formou překladače GNU C Compiler pro různé překládané jazyky). První část diplomové práce se zaměřuje na popis problému, návrh architektury a nástroje, které je možné využít při vývoji. Druhá část je zaměřena na vlastní aplikaci, popis použitých datových struktur a možnosti rozšíření aplikace přidáváním modulů. Poslední část diplomové práce popisuje dosažené výsledky a další směry, které je možné v aplikaci rozvíjet.
|
|
| |
|
|
Using Java PathFinder for Construction of Abstractions of Java Programs
Yuldashev, Nodir ; Parízek, Pavel (vedoucí práce) ; Poch, Tomáš (oponent)
S rostoucí složitostí moderních softwarových systémů se jejich verifikace stává velmi obtížnou úlohou. Techniky formální verifikace a analýzy slouží k nalezení chyb v kódu nebo pro prokázání, že kód splňuje určité vlastnosti. Populární technika automatické verifikace je model checking, který využívá procházení stavového prostoru. Nicméně model checking je náchylný k problému exponenciálního nárustu počtu stavů (state explosion) a proto nemůže být použit pro složité vícevláknové softwarové systémy. Obecné řešení tohoto problému (state explosion) spočívá ve vytvoření abstrakce cílového systému a následném použití tohoto modelu k verifikaci. V rámci diplomové práce jsme navrhli a implementovali nástroj pro konstrukci abstrakce Java komponent v jazyce behavior protocol, který využívá model checker Java PathFinder pro procházení stavového prostoru. Výsledky experimentů na několika netriviálních komponentách ukazují, že nástroj může být použit v praxi.
|
|
|
Checking Compliance of Java Implementation with TBP Specification
Jančík, Pavel ; Parízek, Pavel (vedoucí práce) ; Kofroň, Jan (oponent)
Verifikace je postup umožnující zlepšit spolehlivost aplikací složených z komponent. Jedním z aktuálních témat je kompozice komponent a ověřování, zdali je tato kompozice korektní z pohledu komunikace mezi nimi. Pro popis této komunikace (chování) slouží behavior protokoly (BP). V současné době jsou již vyvinuty nástroje ověřující kompozici komponent. Tyto nástroje ovšem fungují na bázi porovnávání BP a tedy implicitně předpokládají, že implementace komponenty odpovídá danému BP. Odtud vyplývá důležitost nástroje na ověření, zda chování dané implementace odpovídá připojenému BP. Pravidla pro komunikaci komponent společně s BP se obvykle vytvářejí v raných fázích vývojového cyklu. Během implementace typicky dochází k různým ať již úmyslným či neúmyslným, odchylkám od původního návrhu. Tento přístup k vývoji software ještě zvyšuje důležitost ověření, zda aktuální implementace vyhovuje původnímu návrhu BP. Výsledkem práce je nástroj, který ověřuje, zda chování implementace jedné komponenty v jazyce Java odpovídá chování definovanému v připojeném threaded behavior protokolu. Dále práce obsahuje vyhodnocení nástroje na větších příkladech pro nastínění aplikovatelnosti přístupu v praxi.
|
|
|
Automated detection of vulnerabilities in web applications
Tomori, Rudolf ; Parízek, Pavel (vedoucí práce) ; Babka, Vlastimil (oponent)
Významným a častým problémom webových aplikácií sú bezpečnostné chyby, z ktorých vel'ká část' sa dá pomerne presne deterministickým algoritmom identifikovat' pomocou na to určeného špecializovaného softwaru. Nástroj WebCop vyvinutý v rámci tejto práce dokáže lokalizovat' vo webových aplikácíách vybrané bezpečnostné zranitel'nosti. Jeho výhoda oproti bežne dostupnému softwaru spočíva v konfigurovatel'nosti prevádzaných testov, kde samotný užvatel' definuje podmienky urujúce prítomnost' konkrétnej zranitel'nosti. Nástroj je implementovaný v jazyku C++ a je určený pre platformu Unix/Linux.
|
host ::
RSS.