|
|
Generování procesních elementů pro FPGA
Lengál, Ondřej ; Tobola, Jiří (oponent) ; Žádník, Martin (vedoucí práce)
Některé aplikace zpracovávající informace, jako je například monitorování počítačových sítí, vyžadují nepřetržité zpracovávání dat přicházejících vysokou rychlostí. S tím, jak tato rychlost vývojem stále stoupá, je žádoucí, aby bylo zpracovávání dat prováděno pomocí hardwarové implementace. Tato práce navrhuje konfigurační systém transformující uživatelem poskytnutou definici procesních funkcí na VHDL definici hardwarové implementace těchto funkcí. Systém je zaměřen na monitorování síťového provozu ve vysokorychlostních sítích.
|
|
|
Webová aplikace pro správu elektronické knihovny
Kocman, Radim ; Rogalewicz, Adam (oponent) ; Lengál, Ondřej (vedoucí práce)
Cílem této práce je vytvoření webové aplikace pro správu elektronické knihovny, která vytváří webové rozhraní nad programem Calibre. Při tvorbě bylo dbáno na to, aby byl výsledek dále jednoduše rozšiřitelný a přístupný širokému okruhu uživatelů. Základem systému je jazyk PHP a knihovna Nette Framework. Text této práce popisuje kompletní vývojový cyklus aplikace od rozboru současného stavu přes analýzu požadavků, návrh systému a návrh uživatelského rozhraní až po implementační detaily a rozbor testování na vzorku uživatelů.
|
|
|
Funkční verifikace výpočetních jednotek procesoru
Valach, Lukáš ; Lengál, Ondřej (oponent) ; Masařík, Karel (vedoucí práce)
Práce se zaobírá začleněním procesu funkční verifikace do vývojového cyklu návrhu funkčních jednotek v prostředí pro souběžný návrh hardwaru a softwaru systému Codasip. Cílem bylo navrhnout a implementovat verifikační prostředí v jazyku SystemVerilog pro verifikaci automaticky generované hardwarové reprezentace těchto jednotek. Na začátku jsou rozebrány přínosy a obvyklé postupy při funkční verifikaci a vlastnosti systému Codasip. Dále je v práci popsán návrh, implementace, analýza průběhu a výsledků testů verifikace simulačního modelu aritmeticko-logické jednotky. Závěrem jsou zhodnoceny dosažené výsledky práce a navrhnuta zlepšení pro možný další rozvoj verifikačního prostředí.
|
|
|
Efektivní algoritmy pro práci s konečnými automaty
Hruška, Martin ; Rogalewicz, Adam (oponent) ; Lengál, Ondřej (vedoucí práce)
Nedeterministické konečné automaty jsou používány v mnoha oblastech informatiky, mimo jiné také ve formální verifikaci, při návrhu číslicových obvodů nebo pro reprezentaci regulárlních jazyků. Jejich výhodou oproti deterministickým konečným automatům je schopnost až exponenciálně stručnější reprezentace jazyka. Nicméně, tato výhoda může být pozbyta, jestliže je zvolen naivní přístup k implementaci některých operací, jako je na\-pří\-klad test jazykové inkluze dvojice automatů, jehož naivní implementace provádí explicitní determinizaci jednoho z automatů. V nedávné době bylo ale představeno několik nových přístupů, které právě explicitní determinizaci při testu jazykové inkluze předcházejí. Tyto přístupy využívají tzv. antichainů nebo tzv. bisimulace vzhůru ke kongruenci. Cílém této práce je vytvoření efektivní implementace zmíněných přístupů v podobě nového rozšíření knihovny VATA. Vytvořená implementace byla otestována a je až řádově rychlejší v 90% testovaných případů nežli implementace jiné
|
|
|
Efektivní knihovna pro práci s konečnými stromovými automaty
Lengál, Ondřej ; Konečný, Filip (oponent) ; Vojnar, Tomáš (vedoucí práce)
Mnoho současných počítačových systémů používá dynamické datové či řídicí struktury předem neomezené velikosti. Tyto datové struktury mají často charakter stromů nebo se dají zakódovat jako stromy s některými dodatečnými ukazateli nad stromovou kostrou. Této skutečnosti využívají některé v současné době intenzivně studované techniky formální verifikace, které reprezentují nekonečně mnoho stavů konečným stromovým automatem. Nicméně v současnosti neexistuje efektivní a flexibilní implementace knihovny pro stromové automaty, která by byla pro tyto techniky vhodná. Cílem této diplomové práce je takovouto knihovnu poskytnout. Předložený text nejdříve popisuje základy teorie konečných stromových automatů a regulárních stromových jazyků. Dále jsou prozkoumány existující implementace knihoven pro stromové automaty a různé verifikační techniky pro systémy se stromovou strukturou. Poté se text zaobírá návrhem reprezentace stromového automatu a algoritmů provádějících standardní jazykové operace nad touto reprezentací, načež následuje popis implementace knihovny. Prostřednictvím provedených experimentů ukazujeme, že knihovna může konkurovat ostatním dostupným knihovnám pro práci se stromovými automaty, přičemž její výkon v určitých oblastech je řádově vyšší.
|
|
|
Nástroj pro práci s Büchi automaty
Schindler, Petr ; Lengál, Ondřej (oponent) ; Rogalewicz, Adam (vedoucí práce)
Tato práce zpracovává problematiku Büchiho automatů a představuje knihovnu, umožňující provádět základní operace nad těmito automaty. V práci jsou uvedeny základy teorie automatů. Ty jsou použity při popisu konečných automatů, mezi které patří Büchiho automaty, jejichž popis tvoří hlavní část zde uvedené teorie. Znalost jejich vlastností je důležitá pro pochopení algoritmů, které s nimi pracují. Dále jsou tyto algoritmy představeny i s detailním vysvětlením. Následuje návrh datových struktur formátu, v jakém jsou automaty ukládány na disk. Stěžejní část práce se věnuje implementaci knihovny a pomocných skriptů. Detailně jsou zde popsány důležité nebo zajímavé části implementace jednotlivých metod. Závěr práce je věnován testování funkčnosti knihovny.
|
|
|
Simulátor Turingových strojů popsaných pomocí kompozitních diagramů
Siska, Josef ; Lengál, Ondřej (oponent) ; Rogalewicz, Adam (vedoucí práce)
V této práci je uvedena teorie související s Turingovými stroji a formami jejich popisu se zaměřením na kompozitní diagramy. Cílem práce je vytvořit aplikaci, která umožní editaci Turingových strojů zapsaných pomocí kompozitních diagramů a simulaci jejich běhu na zadané vstupní konfiguraci (včetně strojů nedeterministických i vícepáskových). Dále bude aplikace umožňovat spustit analýzu daného Turingova stroje za účelem zjištění, zda tento stroj nebo některé jeho části vždy zastaví. Výsledná aplikace poskytující uvedené funkce je implementována v Javě a zmíněná analýza je v ní prováděna s využitím konstrukce fundovaných uspořádání. V rámci práce tak vznikl nástroj umožňující návrh a testování Turingových strojů zapsaných pomocí kompozitních diagramů. Aplikace může najít své využití zejména při výuce teoretické informatiky, kde může posloužit např. pro demonstraci činnosti daného Turingova stroje.
|
|
|
A Decision Procedure for the WSkS Logic
Fiedor, Tomáš ; Rogalewicz, Adam (oponent) ; Lengál, Ondřej (vedoucí práce)
Various types of logics are often used as a means for formal specification of systems. The weak monadic second-order logic of k successors (WSkS) is one of these logics with quite high expressivity, yet still decidable. Although the complexity of checking satisfiability of a WSkS formula is not even in the ELEMENTARY class, there are approaches to this problem based on deterministic tree automata that perform well in practice, like the MONA tool that efficiently solves the class of practical formulae, but fails for some others. This work extends the class of practically solvable formulae with the use of recently developed techniques for efficient manipulation of non-deterministic automata (such as the antichains algorithm for testing universality) and designs a new decision procedure using non-deterministic automata. The procedure is implemented and is compared with the MONA tool and for some cases yield better results than MONA.
|
|
|
Skrytý souborový systém pro GNU/Linux
Pavlásek, Martin ; Smrčka, Aleš (oponent) ; Lengál, Ondřej (vedoucí práce)
Některá citlivá data vyžadují takový způsob ukrytí, který skryje nejen obsah dat, ale i samotnou jejich existenci. Cílem této bakalářské práce je vytvoření souborového systému, který umožňuje skrývání souborů s citlivými daty do jiných souborů. Práce obsahuje přehled principů používaných v souborových systémech a popis struktury a použití technologie FUSE. Dále je v práci popsán návrh souborového systému skrývajícího souborory do ID3 značek hudebních souborů ve formátu MP3 a jeho implementace v jazyce C++. V závěru práce je vzniklý souborový systém experimentálně ověřen a zhodnocen.
|
|
|
Verifikovaná knihovna datových struktur
Rychnovský, Jan ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
Tato bakalářská práce se zabývá metodikou psaní verifikovaných programů pomocí nástroje VCC. Zmíněná metodika je založena na principu doplnění kódu programu o anotace, jež poskytují specifikaci požadované funkcionality. Nástroj VCC pak prostřednictvím formálních metod určí zda zdrojový kód splňuje danou specifikaci či ne. V první části práce je popsána formální verifikace a zmíněny tři základní přístupy k ní. Následně jsou popsány problémy splnitelnosti výrokových formulí (SAT) a splnitelnosti formulí v teoriích predikátové logiky (SMT). Práce se dále věnuje popisu verifikačního nástroje VCC, jeho funkčnosti, metodice, syntaxi a sémantice příkazů jeho anotačního jazyka BoogiePL. Druhá část textu je zaměřena na popis návrhu a implementace verifikované knihovny datových struktur obsahující jednosměrný, dvousměrný a kruhový seznam, binární vyhledávací strom a Treiberův zásobník. Závěr práce diskutuje získané poznatky o programovací metodice založené na psaní verifikovaného kódu.
|
host ::
RSS.