|
|
OSLC Adapter for ANaConDA Framework
Vašíček, Ondřej ; Kočí, Radek (referee) ; Smrčka, Aleš (advisor)
This work is a proof of concept for adding an OSLC interface to academic software tools. The process of adding OSLC support to a tool is demonstrated by creating an OSLC adapter for the ANaConDA framework using Eclipse Lyo. The goal of this work is to allow ANaConDA to integrate with other tools. An introduction to ANaConDA, OSLC, and Eclipse Lyo is provided along with an overview of the related basic concepts. Then, the design and implementation of the OSLC adapter for ANaConDA is presented. As a result of this work, the process of creating an OSLC adapter is evaluated, and a working implemented OSLC adapter for ANaConDA is presented. Finally, this work features an overview of my past ANaConDA related work which includes implementation of two data race detectors, FastTrack and Eraser.
|
|
|
Bounded Model Checking Using Java PathFinder
Dudka, Vendula ; Češka, Milan (referee) ; Křena, Bohuslav (advisor)
This thesis deals with the application of bounded model checking method for self-healing assurance of concurrency related problems. The self-healing is currently interested in the Java programming language. Therefore, it concetrate mainly on the model checker Java PathFinder which is built for handling Java programs. The verification method is implemented like the Record&Replay trace strategy for navigation through a state space and performance bounded model checking from reached state through the use of Record&Replay trace strategy. Java PathFinder was extended by new moduls and interfaces in order to perform the bounded model checking for self-healing assurance. Bounded model checking is applied at the neighbourhood of self-healing.
|
|
|
Practical Methods of Automated Verification of Concurrent Programs
Fiedor, Jan ; Arcaini, Paolo (referee) ; Farchi, Eitan (referee) ; Vojnar, Tomáš (advisor)
V dnešní době jsou vícevláknové programy běžné a s nimi i chyby v souběžnosti. Během posledních let bylo vytvořeno mnoho technik pro detekci takovýchto chyb, a i přesto mají vývojáři softwaru problém nalézt správné nástroje pro analýzu svých programů. Důvod je jednoduchý, fungující neznamená vždy praktický. Hodně nástrojů implementujících detekční techniky je obtížně použitelných, přizpůsobených pro konkrétní typy programů nebo synchronizace, nebo špatně škálují, aby zvládly analyzovat rozsáhlý software. Pro některé typy chyb v souběžnosti dokonce ani neexistují nástroje pro jejich detekci, i přesto že vývojáři softwaru na tyto chyby často narážejí ve svých programech. Hlavním cílem této práce je navrhnout nové techniky pro detekci chyb ve vícevláknových programech. Tyto techniky by měly být schopny analyzovat rozsáhlé programy, umožnit detekci méně studovaných typů chyb v souběžnosti, a podporovat širokou škálu programů s ohledem na to, jaké programové konstrukce používají.
|
|
|
Practical Methods of Automated Verification of Concurrent Programs
Fiedor, Jan ; Arcaini, Paolo (referee) ; Farchi, Eitan (referee) ; Vojnar, Tomáš (advisor)
V dnešní době jsou vícevláknové programy běžné a s nimi i chyby v souběžnosti. Během posledních let bylo vytvořeno mnoho technik pro detekci takovýchto chyb, a i přesto mají vývojáři softwaru problém nalézt správné nástroje pro analýzu svých programů. Důvod je jednoduchý, fungující neznamená vždy praktický. Hodně nástrojů implementujících detekční techniky je obtížně použitelných, přizpůsobených pro konkrétní typy programů nebo synchronizace, nebo špatně škálují, aby zvládly analyzovat rozsáhlý software. Pro některé typy chyb v souběžnosti dokonce ani neexistují nástroje pro jejich detekci, i přesto že vývojáři softwaru na tyto chyby často narážejí ve svých programech. Hlavním cílem této práce je navrhnout nové techniky pro detekci chyb ve vícevláknových programech. Tyto techniky by měly být schopny analyzovat rozsáhlé programy, umožnit detekci méně studovaných typů chyb v souběžnosti, a podporovat širokou škálu programů s ohledem na to, jaké programové konstrukce používají.
|
|
|
OSLC Adapter for ANaConDA Framework
Vašíček, Ondřej ; Kočí, Radek (referee) ; Smrčka, Aleš (advisor)
This work is a proof of concept for adding an OSLC interface to academic software tools. The process of adding OSLC support to a tool is demonstrated by creating an OSLC adapter for the ANaConDA framework using Eclipse Lyo. The goal of this work is to allow ANaConDA to integrate with other tools. An introduction to ANaConDA, OSLC, and Eclipse Lyo is provided along with an overview of the related basic concepts. Then, the design and implementation of the OSLC adapter for ANaConDA is presented. As a result of this work, the process of creating an OSLC adapter is evaluated, and a working implemented OSLC adapter for ANaConDA is presented. Finally, this work features an overview of my past ANaConDA related work which includes implementation of two data race detectors, FastTrack and Eraser.
|
|
|
Sequence of Tenses in Spanish
Smažíková, Adéla ; Kratochvílová, Dana (advisor) ; Čermák, Petr (referee)
in English Sequence of Tenses in Spanish Key words: sequence of tenses, past tense, relative tenses, simultaneity, posteriority, anteriority The aim of this thesis is to outline sequence of tenses in Spanish language. It is divided into two parts - theoretical and analytical. The first part focuses on the theoretical view of sequence of tenses, its key terms, relative anteriority, simultaneity and posteriority. It also briefly touches on similarities in the Czech language. Then, it focuses on the theoretical tendencies with an impact on the basic rules of sequence of tenses. The second part is dedicated to the practical corpus analysis based on Royal Spanish Academy's corpuses CREA and CORPES XXI. The objective of this analysis is to explore further the frequency of (non)observance of sequence of tenses in combination with the particular verb forms as well as analyse possible reasons of this nonobservance within a specific language material.
|
|
|
Bounded Model Checking Using Java PathFinder
Dudka, Vendula ; Češka, Milan (referee) ; Křena, Bohuslav (advisor)
This thesis deals with the application of bounded model checking method for self-healing assurance of concurrency related problems. The self-healing is currently interested in the Java programming language. Therefore, it concetrate mainly on the model checker Java PathFinder which is built for handling Java programs. The verification method is implemented like the Record&Replay trace strategy for navigation through a state space and performance bounded model checking from reached state through the use of Record&Replay trace strategy. Java PathFinder was extended by new moduls and interfaces in order to perform the bounded model checking for self-healing assurance. Bounded model checking is applied at the neighbourhood of self-healing.
|
|
|
Development of Multithreaded Applications on the Java 8 platform
Souček, Dan ; Pecinovský, Rudolf (advisor) ; Pavlíčková, Jarmila (referee)
This master thesis is a programmer's guide book of a concurrent programming on the Java 8 platform. Concurrency brings additional issues that cannot occur in single-threaded ap-plications. One of the thesis' objectives is to analyze these issues and introduce several principles that, in case they are properly followed, help to create flawless and well-behaving concurrent applications. Another goal of this thesis is to describe the Java con-currency programming from the theoretical point of view. Firstly, the thesis is focused on basic thread development and synchronization issues. Later, it introduces the features and instruments that are provided by Java 5 and higher versions. The theoretical passages are enriched by practical examples that perform discussed features and help to clarify some specific issues. The thesis is written in Czech language and covers large set of concurrency topics from the very basics through the utility libraries to modern instruments present in Java 8.
|
guest ::
