|
|
Adaptér OSLC pro framework ANaConDA
Vašíček, Ondřej ; Kočí, Radek (oponent) ; Smrčka, Aleš (vedoucí práce)
Předmětem této práce je ověření konceptu rozšiřování akademických programových nástrojů o OSLC rozhraní. Proces rozšíření nástroje o OSLC rozhraní je demonstrován vytvořením OSLC adaptéru pro prostředí ANaConDA za použití Eclipse Lyo. Cílem této práce je umožnit integraci prostředí ANaConDA s jinými programovými nástroji. Práce poskytuje základní úvod k prostředí ANaConDA, OSLC a Eclipse Lyo spolu s přehledem souvisejících konceptů. Dále je popsán návrh a implementace vytvořeného OSLC adaptéru. Výsledkem této práce je zhodnocení procesu vytváření OSLC adaptéru a představení implementovaného OSLC adaptéru pro prostředí ANaConDA. Závěrem je zmíněna má předchozí práce na rozšiřování prostředí ANaConDA ve formě implementace dvou detektorů souběhů, FastTrack a Eraser.
|
|
|
Bounded model checking v nástroji Java PathFinder
Dudka, Vendula ; Češka, Milan (oponent) ; Křena, Bohuslav (vedoucí práce)
Diplomová práce je věnovaná aplikaci formální metody bounded model checking pro automatickou opravu chyb. Oprava se specializuje na chyby spojené se souběžností. Práce je zaměřena na programy napsané v jazyce Java, a proto pro verifikační metodu byl zvolen model checker Java Pathfinder, který je určen pro Java programy. Vlastní verifikační metoda spočívá v aplikaci strategie pro navigaci stavovým prostorem do místa verifikace. Z daného místa je spuštěn bounded model checking pro ověření opravy. Navigace stavovým prostorem je implementována pomocí strategie record&replay trace. Pro aplikaci bounded model checkingu jsou implementovány další parametry a moduly pro verifikaci speciálních vlastností systému, které ověřují koreknost opravy chyby. Bounded model checking se provádí v okolí opravy.
|
|
|
Practical Methods of Automated Verification of Concurrent Programs
Fiedor, Jan ; Arcaini, Paolo (oponent) ; Farchi, Eitan (oponent) ; Vojnar, Tomáš (vedoucí práce)
Nowadays, multi-threaded programs are quite common and so are concurrency errors. Over the years, many techniques were developed to detect such errors, yet software developers still struggle to find the right tools to analyse their programs. The reason is simple, working does not always mean practical. Many tools implementing the detection techniques are hard to use, tailored for a specific kind of programs or synchronisation, or do not scale well to handle large software. For some types of concurrency errors, no tools even exist, yet many software developers encounter such errors in their programs. The main goal of this thesis is to develop new techniques for detecting errors in multi-threaded programs. These techniques should be able to handle complex programs, allow one to detect some of the less studied types of concurrency errors, and support a broad variety of programs.
|
|
|
Practical Methods of Automated Verification of Concurrent Programs
Fiedor, Jan ; Arcaini, Paolo (oponent) ; Farchi, Eitan (oponent) ; Vojnar, Tomáš (vedoucí práce)
Nowadays, multi-threaded programs are quite common and so are concurrency errors. Over the years, many techniques were developed to detect such errors, yet software developers still struggle to find the right tools to analyse their programs. The reason is simple, working does not always mean practical. Many tools implementing the detection techniques are hard to use, tailored for a specific kind of programs or synchronisation, or do not scale well to handle large software. For some types of concurrency errors, no tools even exist, yet many software developers encounter such errors in their programs. The main goal of this thesis is to develop new techniques for detecting errors in multi-threaded programs. These techniques should be able to handle complex programs, allow one to detect some of the less studied types of concurrency errors, and support a broad variety of programs.
|
|
|
Adaptér OSLC pro framework ANaConDA
Vašíček, Ondřej ; Kočí, Radek (oponent) ; Smrčka, Aleš (vedoucí práce)
Předmětem této práce je ověření konceptu rozšiřování akademických programových nástrojů o OSLC rozhraní. Proces rozšíření nástroje o OSLC rozhraní je demonstrován vytvořením OSLC adaptéru pro prostředí ANaConDA za použití Eclipse Lyo. Cílem této práce je umožnit integraci prostředí ANaConDA s jinými programovými nástroji. Práce poskytuje základní úvod k prostředí ANaConDA, OSLC a Eclipse Lyo spolu s přehledem souvisejících konceptů. Dále je popsán návrh a implementace vytvořeného OSLC adaptéru. Výsledkem této práce je zhodnocení procesu vytváření OSLC adaptéru a představení implementovaného OSLC adaptéru pro prostředí ANaConDA. Závěrem je zmíněna má předchozí práce na rozšiřování prostředí ANaConDA ve formě implementace dvou detektorů souběhů, FastTrack a Eraser.
|
|
|
Souslednost časová ve španělštině
Smažíková, Adéla ; Kratochvílová, Dana (vedoucí práce) ; Čermák, Petr (oponent)
v českém jazyce Souslednost časová ve španělštině Klíčová slova: souslednost časová, minulý čas, relativní časy, souběžnost, následnost, předčasnost Tato práce se zabývá sousledností časovou ve španělštině. Je rozdělena na část teoretickou a část praktickou. V první části práce se teoreticky věnujeme problematice souslednosti časové, vymezujeme stěžejní pojmy, zaměřujeme se na relativní předčasnost, souběžnost a následnost a stručně nastiňujeme i situaci v češtině. Dále se teoreticky zabýváme tendencemi v jazyce, které mohou mít dopad na obecná pravidla souslednosti časové. Druhá část je věnována praktické korpusové analýze, pro kterou využíváme korpusy Španělské královské akademie CREA a CORPES XXI. Cílem naší analýzy je prostudovat četnost (ne)dodržení souslednosti časové po konkrétních slovesných formách a dále analyzovat možné důvody jejího nedodržení na konkrétním jazykovém materiálu.
|
|
|
Bounded model checking v nástroji Java PathFinder
Dudka, Vendula ; Češka, Milan (oponent) ; Křena, Bohuslav (vedoucí práce)
Diplomová práce je věnovaná aplikaci formální metody bounded model checking pro automatickou opravu chyb. Oprava se specializuje na chyby spojené se souběžností. Práce je zaměřena na programy napsané v jazyce Java, a proto pro verifikační metodu byl zvolen model checker Java Pathfinder, který je určen pro Java programy. Vlastní verifikační metoda spočívá v aplikaci strategie pro navigaci stavovým prostorem do místa verifikace. Z daného místa je spuštěn bounded model checking pro ověření opravy. Navigace stavovým prostorem je implementována pomocí strategie record&replay trace. Pro aplikaci bounded model checkingu jsou implementovány další parametry a moduly pro verifikaci speciálních vlastností systému, které ověřují koreknost opravy chyby. Bounded model checking se provádí v okolí opravy.
|
|
|
Možnosti vývoje vícevláknových aplikací na platformě Java 8
Souček, Dan ; Pecinovský, Rudolf (vedoucí práce) ; Pavlíčková, Jarmila (oponent)
Tato diplomová práce je programátorskou příručkou pro vývoj vícevláknových aplikací na platformě Java 8. Vícevláknové programování přináší řadu problémů, které se v jednovláknových aplikacích nevyskytují. Jedním z cílů této práce je rozebrat tyto problémy a na jejich základě uvést zásady, které je nutné dodržovat, aby vícevláknové aplikace fungovaly správně. Dalším cílem je teoreticky popsat, jak programovat vícevláknové aplikace v jazyce Java. Nejprve se práce věnuje základům programování vláken a synchronizaci, poté je zaměřena na vývojové nástroje, které poskytují verze Java 5 a vyšší. Teoretický popis jednotlivých funkcionalit je doplněn praktickými ukázkami kódu, který demonstruje použití předvedených nástrojů a lépe vysvětluje danou problematiku. Přínosem této práce je, že je napsána v českém jazyce a pokrývá širokou oblast vícevláknového programování od základů přes užitečné sady knihoven až po nejmodernější nástroje Javy 8. Klíčová slova
|
host ::
RSS.