|
|
Verifikace za běhu systémů s vlastnostmi v MTL logice
Olšák, Ondřej ; Hruška, Martin (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato práce se zabývá návrhem algoritmu pro ověřování splnitelnosti omezení programu zapsaných pomocí metrické temporální logiky (MTL), kdy sledování splnitelnosti těchto formulí probíhá za běhu daného programu. K ověřování těchto vlastností využívá navržený algoritmus stromové struktury, která je podobná chování alternujícího časového automatu, ze kterého je výsledný postup sledování programu odvozen. Navržený algoritmus, je schopen za běhu daného programu ověřovat jeho vlastnosti vůči definovaným MTL formulím a to bez potřeby pamatovat si stavy, ve kterých se sledovaný program nacházel. To umožňuje ověřit vlastnosti daného programu u potenciálně nekonečných běhů.
|
|
|
Support of Run-time Monitoring of Processes in ANaConDA Framework
Mužikovská, Monika ; Rogalewicz, Adam (oponent) ; Smrčka, Aleš (vedoucí práce)
This work extends ANaConDA framework for dynamic analysis of multi-threaded programs with support for multi-process monitoring. This thesis summarizes ANaConDA's approach to analysis and differences between threads and processes. The most important ones involve inter-process communication, separate logical address spaces, and synchronisation with general semaphores. The implemented extension provides API for inter-process communication via shared memory, monitors operations with shared memory in order to translate virtual addresses to their unique representation among processes, and monitors synchronisation operations with semaphores and provides information about them to analysers. The extension significantly simplifies the development of multi-process analysers. This is shown on implementation of two analysers for data race detection, AtomRace and FastTrack, which were, until now, available for multi-threaded programs only. The implementation of FastTrack algorithm uses happens-before relation for general semaphores which is also defined in this thesis. Proposed and implemented solutions were verified on a set of automatic tests and the two analysers were used for experiments on a set of students' projects. Experiments showed that ANaConDA framework is now able to detect concurrency-related errors in multi-process programs and, as such, provide support with implementation of large category of parallel programs.
|
|
|
Internetový robot plnící funkci kalendáře
Klos, Jakub ; Očenášek, Pavel (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato bakalářská práce se zabývá vytvořením internetového robota, který funguje jako správce kalendáře událostí. Robot s uživatelem komunikuje pomocí podmnožiny přirozeného anglického jazyka. Uživatel se nemusí učit speciální syntaxi příkazů a používání robota-kalendáře je mu tak maximálně usnadněno, což je hlavním přínosem této práce. Tento způsob ovládání by měl pomoci zejména počítačově méně zdatným uživatelům, pro které by ovládání speciálními příkazy mohlo být překážkou. Pro komunikaci, která se odehrává formou instant messagingu, je využit protokol XMPP. Ke strojovému zpracování přirozeného jazyka bylo využito nástroje NLTK. Program robota byl kompletně vytvořen v programovacím jazyce Python. Práce se také zabývá dalšími možnostmi rozšiřování funkcionality robota.
|
|
|
Instrumentace Java programů, kontrakty pro paralelismus
Žárský, Jan ; Křena, Bohuslav (oponent) ; Smrčka, Aleš (vedoucí práce)
Kontrakty pro paralelismus slouží k vyjádření potřebné atomicity sekvencí metod ve vícevláknových programech. Tato práce se zaměřuje na implementaci dynamického analyzátoru, který verifikuje programy napsané v jazyce Java vůči kontraktům. Podporovány jsou parametrické kontrakty se spojlery. Analyzátor je implementován jako rozšíření frameworku RoadRunner. V rámci implementace analyzátoru byla do frameworku RoadRunner přidána podpora pro získávání argumentů metod a jejich návratových hodnot. Analyzátor byl plně implementován a jeho funkčnost byla ověřena na sadě testovacích programů.
|
|
|
Pro lidi srozumitelný jazyk temporální logiky
Žilka, Lukáš ; Letko, Zdeněk (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato práce se zabývá automatickým překladem z přirozeného jazyka do temporální logiky. Existující výzkum na toto téma je shrnut a práce je na něm založena. Pro specifikaci temporálních vlastností, je vytvořen kontrolovaný jazyk, podmnožina anglického jazyka. Hlavním přínosem práce jsou algoritmy pro překlad mezi přirozeným jazykem a temporální logikou, založený na zpracovávání a prohledávání vzorů v gramatických závislostech Standfordského parseru angličtiny. Další směr vývoje je diskutován na konci.
|
|
|
Dynamická analýza použití knihovních volání
Malík, Viktor ; Peringer, Petr (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato bakalářská práce se zabývá vývojem dynamického analyzátoru, který sleduje používání knihovních volání analyzovaným programem. Analyzátor dále tato volání automaticky ovládá za účelem vytváření různých běhů programu, které pak agreguje do výsledného grafu toku řízení. Pro sledovaní a ovládání volání používá analyzátor vlastní sdílenou knihovnu pro operační systém GNU/Linux. Součástí práce je jak podrobný návrh celé aplikace, tak i její implementace v~jazycích C/C++ zaměřující se na sledování standardních knihovních volání nad souborovým systémem.
|
|
|
Automatické konfigurování služeb operačního systému
Schiffer, Peter ; Peringer, Petr (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato diplomová práce se zabývá konfigurací operačních systémů, jejich možnostmi a způsoby nastavení. Představuje rozdíly v konfiguraci operačních systémů podle jejich zaměření a pokročilé možnosti konfigurace operačních systémů pomocí aplikací třetích stran. Praktická část diplomové práce se zabývá návrhem nového počítačového jazyka zaměřeného na popis konfigurace operačního systému a jeho služeb. Tento popis konfigurace sloužící na automatickou konfiguraci systémových služeb se překládá na sekvenci konfiguračních příkazů. Výhoda jazyka spočívá v jeho dobré čitelnosti pro člověka, ale podobnost s přirozeným jazykem přináší určitou úroveň nejednoznačnosti. Navrhovaná metoda automatického generování příkazů řeší nejednoznačnost vyhledáváním co nejméně destruktivního řešení v podobě kombinaci konfiguračních příkazů.
|
|
|
Application for OpenShift Plaform for Testing of Students Projects
Országh, Marián ; Janoušek, Vladimír (oponent) ; Smrčka, Aleš (vedoucí práce)
The aim of this thesis is to design a service for automated requirements-based testing of student programming assignments, and thereafter implement this service using the OpenShift, Python and Git technologies. By creating such a service, a foundation is set for a unified testing process, which includes executing the test suites in separate Linux containers. Such a process is intended for simplification of the grading by teachers and teacher assistants, and at the same time improvement of student's performance in such tasks. This Master's thesis explains the basics of software testing, while focusing on requirements-based testing specifically. Furthermore, it provides insight into the container technology, as well as how these themes are applied in the project's design, and how they are reflected in the service's requirements. Afterwards, the implementation details of the service are put under examination in order to provide a reference material for any future extensions of the project. The implemented service allows for basic operations, including testing of multiple student projects in separate containers concurrently, creating a containerized debugging session, or automatically building a testing container image for a given assignment.
|
|
|
Nástroj pro podporu tvorby automatické testovací sady
Studený, Martin ; Rogalewicz, Adam (oponent) ; Smrčka, Aleš (vedoucí práce)
Cílem bakalářské práce je vytvořit nástroj Suiter , který testerovi zjednoduší a částečně zautomatizuje proces tvorby testovacích skriptů v širokém spektru programovacích jazyků. Důraz je kladen na testování rozhraní pro programování aplikací ( API ) kombinováním vstupních hodnot v určitém stavu webové aplikace. Aplikace Suiter generuje spustitelnou sadu testů uspokojující požadovaná kombinační kritéria. Výsledky této práce umožňují testerům zrychlit a zefektivnit testování API .
|
|
|
Optimalizace platformy pro distribuované výpočty Hadoop
Čecho, Jaroslav ; Smrčka, Aleš (oponent) ; Letko, Zdeněk (vedoucí práce)
Tato diplomová práce se zabývá možnostmi optimalizace frameworku Hadoop za pomocí platformy CUDA. Apache Hadoop je frameworku umožnující analýzu obrovských objemů dat. Obsahuje distribuovaný souborový systém a implementaci programovacího paradigmatu mapreduce s jehož pomocí se poté píší uživatelské aplikace. Platforma CUDA firmy NVIDIA umožnuje využít výkon grafické karty počítače i k jiným účelům než je generování grafického výstupu na zobrazovací zařízení počítače. Má prace obsahuje seznam a experimentální implementaci výpočtů frameworku Hadoop vhodných k přesunu z hlavního procesoru počítače na grafickou kartu za účelem dosáhutí časové optimalizace běžících mapreduce aplikací.
|
host ::
RSS.