|
|
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)
|
|
|
Domain-Specific Language for Learning Programming
Klimeš, Jonáš ; Parízek, Pavel (vedoucí práce) ; Vinárek, Jiří (oponent)
V rámci této práce jsme navrhli jazyk pro výuku programování. Nejprve jsme popsali osm existujících nástrojů pro výuku programování a identifikovali jsme jejich vlastnosti, které jsou důležité pro proces učení. Potom jsme navrhli výukový doménově specifický jazyk Eddie. Eddie je vhodný pro dospívající děti a dospělé, kteří se chtějí naučit programovat. Jazyk používá doménu postavenou na jazyku Robot Karel, ve které uživatelé mohou ovládat postavičku robota ve dvourozměrné mřížce. Vytvořili jsme prototyp jazyka Eddie pomocí nástroje MPS Language Workbench. Jazyk Eddie postupně představuje cykly, podmínky, proměnné, funkce a objekty. Uživatelské programy mohou být vytvářeny a spouštěny ve vývojovém prostředí Eddie Studio. Eddie Studio také vizualizuje akce robota ve spuštěném programu. Powered by TCPDF (www.tcpdf.org)
|
|
|
Static analysis of C# programs
Malý, Petr ; Bednárek, David (vedoucí práce) ; Parízek, Pavel (oponent)
Cílem této diplomové práce je prozkoumat a aplikovat jednotlivé metody statické analýzy C# programů přeložených do Common Intermediate Language. Výsledky této práce jsou zakomponovány do systému ParallaX Development Envrionment. Tato diplomová práce se zaměřuje na Structural, Points-to a Dependence Analysis. Powered by TCPDF (www.tcpdf.org)
|
|
|
Bobox Runtime Optimization
Krížik, Lukáš ; Zavoral, Filip (vedoucí práce) ; Parízek, Pavel (oponent)
Cílem této diplomové práce je vytvořit nástroj na optimalizaci kódu pro paralelní prostředí Bobox. Nástroj redukuje počet krátce a dlouze běžících úloh na základě statické analýzy kódu. Některé případy krátce běžících úloh způsobují zbytečné přeplánování. Pokud plánovač nemá dostatek informací o dané úloze, plánovač může úlohu naplánovat, i když tato úloha nemá všechna potřebná vstupní data. Pro odstranění krátce běžící úlohy nástroj analyzuje použití vstupních dat a informuje plánovač. Dlouze běžící úlohy můžou v některých případech potlačit paralelismus. Větší granularita úloh může znatelně vylepšit časy běhu v paralelním prostředí. Pro odstranění dlouze běžících úloh nástroj musí být schopen vyhodnotit složitost kódu a vložit příkaz pro přeplánování na vhodné místo. Powered by TCPDF (www.tcpdf.org)
|
|
|
Context Aware Android Application Trace Analysis
Kacz, Kristián ; Pop, Tomáš (vedoucí práce) ; Parízek, Pavel (oponent)
Diplomová práce prozkoumává podporu context-aware aplikací v současných mobilních operačních systémech a vyšetřuje možnosti debugování mobilních aplikací. Práce poukazuje na problémy vyskytující se při debugování context-aware aplikací. Hlavním cílem práce je nejdříve navrhnout debugovací metodu, která bere do úvahy kontextové informace, a pak tuto metodu naimplementovat. Součástí práce je i příklad použití z reálného světa, která demonstruje navrhnutou metodu.
|
|
|
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.
|
|
|
Source Code Similarity Detection
Lano, Radek ; Parízek, Pavel (oponent) ; Tůma, Petr (vedoucí práce)
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.
|
|
|
Regression Benchmarking Web
Babka, David ; Parízek, Pavel (oponent) ; Tůma, Petr (vedoucí práce)
Při vývoji software je jeho výkon často důležitou součástí požadavků zákazníka. Vzhledem k tomu, že se software neustále vyvíjí, lze pomocí porovnávání výsledků testů výkonu určit nedostatky ve zdrojovém kódu a tím celkově optimalizovat výkon software. Tato práce se zabývá implementací flexibilní webové aplikace založené na získávání těchto výsledků a jejich prezentací je v grafech a jiných formách. Pro co nejlepší přehlednost bude možné tyto grafy dynamicky generovat. Další z výhod této aplikace bude možnost zasílání e-mailů uživatelům s informacemi o nových měřeních.
|
|
|
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...
|
|
|
Interoperability between component-based and service-oriented systems
Mašek, Karel ; Hnětynka, Petr (vedoucí práce) ; Parízek, Pavel (oponent)
Pro vývoj a návrh rozsáhlých softwarových systémů, se používají převážně dva přístupy: komponentový a servisně-orientovaný návrh. V systémech, kde se oba přístupy kombinují, je interoperabilita (t.j. jejich vzájemná spolupráce) klíčovou vlastností. Cílem práce je navrhnout a experimentálně implementovat řešení pro interoperabilitu mezi komponentovým systémem SOFA2 a servisně orientovanou platformou OSGi. Výsledné řešení je založené na použití aspektů a annotací. Annotace slouží k deklarativnímu označení komponent, které využívají (t.j. volají nebo publikují) OSGi servisy. Naopak, pomocí aspektů se označeným komponentům poskytne OSGi funkcionalita, t.j. kontrolní logika. Kromě komponentového systému SOFA2, byla podpora pro OSGi přidána i do nástroje, který slouží pro vývoj SOFA2 aplikací. Navržené řešení je použitelné nejen pro integraci SOFA2 a OSGi, ale i obecně pro komponentové a servisně-orientované systémy.
|
host ::
RSS.