|
|
Automatizované metody hledání chyb v překladačích
Müller, Petr ; Smrčka, Aleš (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tato práce se zabývá aplikací metody fuzz testing k testování překladačů a interpretů. V první části pojednává o překladačích, optimalizacích a chybách typických pro optimalizující překladač. Analyzuje vhodnost metod statické a dynamické analýzy pro hledání těchto chyb a jako vhodnou navrhuje dynamickou metodu fuzz testování. V rámci práce byl implementován nástroj pro testování překladačů používající tuto metodu, který byl aplikován na několik případů, přičemž se podařilo nalézt sérii chyb v rozšířených překladačích, a to včetně např. GCC.
|
|
|
Nástroj pro vyvolávání chyb založený na infrastrukuře Systemtap
Zelinka, Martin ; Smrčka, Aleš (oponent) ; Vojnar, Tomáš (vedoucí práce)
Práce popisuje různé metody vkládání chyb, princip systémových volání v operačním systému Linux a nástroj Systemtap. Hlavním cílem práce je návrh a implementace aplikace pracující na principu vkládání chyb do systémových volání pomocí nástroje Systemtap. Realizovaná aplikace si nejprve automaticky identifikuje existující systémová volání s jejich chybovými návratovými hodnotami, kterými jsou potom nahrazovány původní návratové hodnoty systémových volání.
|
|
|
Techniky virtualizace výpočetních platforem v Linuxu
Župka, Jiří ; Kumpošt, Marek (oponent) ; Vojnar, Tomáš (vedoucí práce)
Práce testuje a porovnává nástroje pro virtualizaci výpočetních platforem a vysvětluje pojmy důležité pro pochopení problematiky virtualizace. Jejím hlavním přínosem je srovnání s pohledu výkonnosti, efektivnosti, škálovatelnosti a robustnosti virtualizačních nástrojů. Toto srovnání má pomoci firmě Redhat rozhodnout, zda opustit XEN jako hlavní virtualizační nástroj v jejich distribucích a přejít na jiný novější, uživatelsky příjemnější virtualizační nástroj, jako je například KVM.
|
|
|
Statická analýza možných hodnot proměnných v programech v C
Ďuričeková, Daniela ; Peringer, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
Analýza rozsahu hodnot (anglicky value-range analysis) je metoda statické analýzy založená na zjišťování hodnot, kterých může daná proměnná nabývat v určitém místě v programu. Tato technika může být použita k dokázání, že se v programu nevyskytují chyby za běhu, jako například přístup za hranici pole. Jelikož analýza rozsahu hodnot získává informace o každém místě v programu, lze k její implementaci využít analýzu toku dat (anglicky data-flow analysis). Cílem této diplomové práce je návrh a implementace funkčního nástroje provádějícího analýzu rozsahu hodnot. Práce začíná úvodem do problematiky, vysvětlením analýz toku dat a hodnot proměnných a popisem abstraktní interpretace, která tvoří formální základ analyzátoru. Následuje seznámení s prostředím Code Listener, které bylo využito k implementaci analyzátoru. Jádro práce tvoří návrh, implementace a otestování analyzátoru. V závěru jsou shrnuty nabyté zkušenosti a diskutovány možnosti budoucího vývoje vytvořeného nástroje.
|
|
|
Model checking nekonečně stavových systémů založený na inferenci jazyků
Rozehnal, Pavel ; Křena, Bohuslav (oponent) ; Vojnar, Tomáš (vedoucí práce)
Regulární model checking je metoda pro verifikaci nekonečně stavových systémů. Je založena na kódování jejich konfigurace jako slov nad konečnou abecedou, množiny konfigurací jako konečného automatu a přechodů jako konečných transducerů. Je zde představen nový přístup k regulárnímu model checkingu založený na odvozování regulárních jazyků. Metoda je založena na prozkoumávání nekonečně stavového systému, jehož chování může být modelováno použitím transducerů, které zachovávají délku řetězců a jejich aplikací je možné získat všechny dosažitelné konfigurace systému. Naše metoda regulárního model checkingu je založena na odvozování regulárních jazyků pomocí algoritmu Angluin, který je použit pro nalezení vhodného invariantu (nadaproximace), který je schopen zodpovedět otázku zachování či porušení nějaké vlastnosti. Je zde také uveden úvod do teorie konečných automatů, model checkingu, SAT problémů a popis Angluinova a Biermanova algoritmu pro učení konečných automatů.
|
|
|
Mikrojádra operačních systémů
Beneš, Eduard ; Peringer, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
Táto práca sa zaoberá problematikou mikrojadier operačných systémov. Prvá časť je zameraná na oboznámenie s problematikou jadier operačných systémov. Obsahuje základné vlastnosti a mechanizmy druhej generácie mikrojadier reprezentovanej mikrojadrom L4, na ktoré sa zameriavame v ďalších častiach práce. Následne sú opísané dva rôzne porty operačného systému Linux nad mikrojadro L4, sú to L4Linux a Wombat. V druhej časti práce je popísaný spôsob inštalácie vybraných portov a hlavné problémy, ktoré sme museli riešiť. Tretia a štvrtá časť sú zamerané na problematiku testovania výkonnosti nainštalovaných systémov. Popisujeme metodológiu zvolených experimentov a význam jednotlivých testov. Výsledky, spolu s ich vyhodnotením, sú uvedené vo štvrtej časti. Pokiaľ to je vhodné, získané výsledky konfrontujeme medzi sebou, prípadne s výsledkami testov získaných z Internetu. V záverečnej časti je na základe nadobudnutých znalostí uvedená stručná diskusia na tému možností uplatnenia mikrojadier.
|
|
|
SELinux Policy Analysis Tool
Mojžíš, Vít ; Peringer, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis deals with mandatory access control (MAC)-based security module policy analysis, focusing on SELinux. Because of insuffient capabilities of available analysis tools, new tool was designed and implemented with the needs of Red Hat SELinux team in mind. Its main uses will be as aid in policy development and support in SELinux usefulness evaluation. If the tool proves useful, it will be incorporated into SELinux userspace tools package SETools 4.
|
|
|
Refactoring and Verification of the Code of mkfs xfs
Ťulák, Jan ; Peringer, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
This work describes the processes of refactoring mkfs.xfs program for a purpose of refining its code and cleaning the technical debt accumulated over 20 years of the program’s existence. The mkfs.xfs source code is then a subject to static analysis and the used tools (CppCheck, Coverity, Codacy, GCC, Clang) are compared in terms of the number and type of the found defects.
|
|
|
Reportovací nástroj nad git
Nečas, Vojtěch ; Hruška, Martin (oponent) ; Vojnar, Tomáš (vedoucí práce)
Bakalářská práce se zabývá implementací softwarového nástroje pro vytváření a vizualizaci statistických informací o práci v souborech, které sleduje systém správy verzí - Git. Systém Git nemá funkce pro grafické znázornění statistik (grafem nebo tabulkou) a výstup informací o změnách v souborech je pouze v příkazovém řádku. Taková data, zejména u velkého počtu sledovaných souborů, není snadné analyzovat bez použití jiných existujících statistických nástrojů. Existuje několik nástrojů, které umí získat informace o změnách v Git, vyhodnotit statistiky a zobrazit výsledky. Hlavním problémem u těchto nástrojů je příliš dlouhá doba potřebná pro získání výsledků, podpora jen velmi stručných statistik nebo slabé uživatelské rozhraní. Nástroj implementovaný v této práci řeší efektivnější vyhodnocení výsledků pomocí databáze pro uložení informací o změnách z Git. Databáze oproti příkazovému řádku poskytuje rychlý přístup k uloženým informacím a časově náročné je pouze její založení. Snadné ovládaní nástroje zajišťuje grafické uživatelské rozhraní pomocí oken. Výsledkem jsou statistiky, které si může uživatel i přizpůsobit podle vlastních potřeb (která data budou zahrnuta a jejich rozsah). Navíc nástroj poskytuje přibližný odhad (matematicko-statistickou metodou nejmenších čtverců), jakým směrem se práce ve sledovaném projektu ubírá (zda je ve fázi vývoje, nebo dokončování a údržby).
|
|
|
Sdílená tabule
Řezník, Jaroslav ; Mazal, Zdeněk (oponent) ; Vojnar, Tomáš (vedoucí práce)
Cílem projektu "Sdílená tabule" je navrhnout a implementovat aplikaci, která umožní spolupráci na skupinových projektech v reálném čase v síťovém prostředí. Komunikace může probíhat jak pomocí textových zpráv, tak multimediálně pomocí kreslení na sdílené tabuli, vkládáním interaktivních objektů a hlasovou či video komunikací. V rámci semestrální části projektu se řeší využití interaktivních tabulí, návrh komunikačního protokolu a grafického uživatelského rozhraní. V diplomové práci následně implementace aplikace.
|
host ::
RSS.