|
|
Runtime Verification of Systems with MTL Properties
Olšák, Ondřej ; Hruška, Martin (referee) ; Smrčka, Aleš (advisor)
This work is focused on the design of an algorithm for run-time verification over requirements given as formulas in metric temporal logic (MTL). Tree structure is used for verification of these requirements, which is similar to run of alternating timed automata from which the final algorithm is derivated. Designed algorithm is able to verify given MTL formulas over the runs of a program without a need to remember the whole program's trace. This allows to monitor a given program on potentially infinite runs.
|
|
|
Support of Run-time Monitoring of Processes in ANaConDA Framework
Mužikovská, Monika ; Rogalewicz, Adam (referee) ; Smrčka, Aleš (advisor)
Tato práce rozšiřuje nástroj ANaConDA pro dynamickou analýzu vícevláknových programů o možnost analyzovat také programy víceprocesové. Část práce se soustředí na popis nástroje ANaConDA a mechanismů, které pro monitorování využívá, a na jejich nutné úpravy vzhledem k rozdílům procesů a vláken. Tyto zahrnují nutnost složitějších mechanismů pro meziprocesovou komunikaci, nutnost překládat logické adresy na jiný jednoznačný identifikátor a monitorování obecných semaforů. Rozšíření pro monitorování procesů tyto problémy řeší za vývojáře analyzátorů, čímž velmi zjednodušuje jejich vývoj. Užitečnost rozšíření je ukázána na implementaci dvou analyzátorů pro detekci souběhu (AtomRace a FastTrack), které bylo dosud možné využít pouze na vícevláknové programy. Implementace algoritmu FastTrack využívá happens-before relaci pro obecné semafory, která byla také definována jako součást této práce. Experimenty s analyzátory na studentských projektech ukázaly, že nástroj ANaConDA je nyní schopen detekovat paralelní chyby i ve víceprocesových programech a může tak pomoci při vývoji další skupiny paralelních programů.
|
|
|
Internet Robot for an Assistance of Calendar Scheduling
Klos, Jakub ; Očenášek, Pavel (referee) ; Smrčka, Aleš (advisor)
This bachelor thesis deals with the development of the internet robot for assistance of calendar scheduling. The robot and a user comunicate with a subset of English. User does not have to study special syntax of the orders which makes using of the robot-calendar much simplier. This easement is the main contribution of the work. This kind of control should help especially to the users with lesser amount of computer skills, for whom the special syntax-oriented-control might be difficult. The XMPP protocol is used for a comunication which is of instant messaging type. NLTK toolkit was used for natural language processing. The source code of the robot is completely programmed in Python programming language. The work also deals with possibilities of robot's further development.
|
|
|
Parametric Contracts for Concurrency in Java Programs
Žárský, Jan ; Křena, Bohuslav (referee) ; Smrčka, Aleš (advisor)
Contracts for concurrency describe required atomicity of method sequences in concurrent programs. This work proposes a dynamic analyzer to verify programs written in Java against contracts for concurrency. The analyzer was designed to detect violations of parametric contracts with spoilers. The proposed analyzer was implemented as an extension to the RoadRunner framework. Support for accessing the method arguments and return values was added to RoadRunner as a part of the solution. The analyzer was fully implemented and verified on a set of testing programs.
|
|
|
Temporal Logics for a Man
Žilka, Lukáš ; Letko, Zdeněk (referee) ; Smrčka, Aleš (advisor)
The work deals with the automated translation of a natural language to temporal logic. Existing research attempts are summarized and built upon. For specificating the temporal properties a subset of English is introduced. The main contribution of the work is the proposed algorithm of translation of a property in the given language to LTL temporal logic, based on processing of and finding patterns in grammatical dependencies of The Stanford English Parser. Future research directions are discussed at the end.
|
|
|
Dynamic Analysis of Programs Using Library Calls
Malík, Viktor ; Peringer, Petr (referee) ; Smrčka, Aleš (advisor)
The objective of this bachelor's thesis is development of dynamic software analysis which monitors library calls of analysed program. The proposed analyser doubles library call routines in order to create different program runs. These runs are then aggregated into a single control flow graph which can be used for subsequent program analysis. Monitoring and controlling the calls is realised via stubs and wrappers encapsulated within a dynamic shared library for GNU/Linux operating system. The proof of concept is shown on dynamic analyser focused on file system library calls.
|
|
|
An Automatic Configuration of Services of Operating System
Schiffer, Peter ; Peringer, Petr (referee) ; Smrčka, Aleš (advisor)
This Master thesis describes the configuration of operating systems and their capabilities. It introduces differences between configuration of different operating systems according to their specialization, and it introduces advanced configuration of operating systems with third-party applications. The practical part of the thesis is a design of a new computer language aimed at describing a configuration of an operating system and its services. Such a description is used to automatically configure system services by translating it to a sequence of configuration commands. An advantage of the language is its readability by a human, but its similarity with natural languages introduces a certain level of ambiguity. The proposed method of automatic generation of commands deals with the ambiguity by searching and selecting as least as possible destructive commands.
|
|
|
Application for OpenShift Plaform for Testing of Students Projects
Országh, Marián ; Janoušek, Vladimír (referee) ; Smrčka, Aleš (advisor)
Cieľom tejto práce je navrhnúť službu pre automatizované testovanie študentských programovacích projektov na základe požiadaviek a následne implementovať túto službu za použitia technológií OpenShift, Python a Git. Vytvorenie takejto služby stavia základ pre zjednotený proces testovania študentských projektov, ktorý zahŕňa spúšťanie testovacích sád v oddelených Linuxových kontajneroch. Vylepšený testovací proces má viesť ku zjednodušeniu známkovania vyučujúcimi a taktiež zlepšeniu výsledkov študentov pri týchto úlohách. Táto diplomová práca vysvetľuje základy testovania softvéru, pričom sa sústredí na testovanie založené na požiadavkách, poskytuje náhľad do technológie kontajnerov a objasňuje, ako boli tieto témy zahrnuté pri návrhu služby a taktiež, ako sa ich použitie odrazilo na požiadavkách na ňu. Okrem toho je implementácia tejto služby podrobená detailnej analýze, ktorá má slúžiť ako referenčný materiál pre jej akékoľvek budúce rozšírenia. Implementovaná služba je schopná vykonávať základné operácie, zahřňajúce paralelné testovanie študentských projektov v oddelených kontajneroch, vytvorenie kontajnerizovaného ladiaceho prostredia, alebo automatické zostavenie kontajnerového obrazu pre konkrétne zadanie.
|
|
|
Tool Supporting Generation of Automatic Test Set
Studený, Martin ; Rogalewicz, Adam (referee) ; Smrčka, Aleš (advisor)
The goal of this bachelor's thesis is to create a Suiter tool that partially automates the process of creating test scripts in a wide range of programming languages . The focus is given to a testing of application programming interface ( API ) by combining input values in a specific state of a web application . Suiter generates an executable set of tests that satisfy the required combination criteria .
|
|
|
Optimization of the Hadoop Platform for Distributed Computation
Čecho, Jaroslav ; Smrčka, Aleš (referee) ; Letko, Zdeněk (advisor)
This thesis is focusing on possibilities of improving the Apache Hadoop framework by outsourcing some computation to a graphic card using the NVIDIA CUDA technology. The Apache Hadoop software library is a framework that allows for the distributed processing of large data sets across clusters of computers using a simple programming model called mapreduce. NVIDIA CUDA is a platform which allows one to use a graphic card for a general computation. This thesis contains description and experimental implementations of suitable computation inside te Hadoop framework that can benefit from being executed on a graphic card.
|
guest ::
