|
|
Jabber/XMPP transport pro diskuzní skupiny přístupné protokolem NNTP
Halfar, Patrik ; Weiss, Petr (oponent) ; Rychlý, Marek (vedoucí práce)
Tato práce se zabývá problematikou výměny informací v počítačových sítích. V první části se zabývá úvodem do diskuzních skupin, známých též pod názvem NetNews a shrnutím hlavních informací o nově se rozvíjejícím projektu Jabber/XMPP . V druhé části jsou popsány možnosti propojení těchto dvou protokolů; a detailněji popisuje aplikaci vytvořenou k tomuto účelu. V příloze je pak uvedeno, jak nakonfigurovat nejznámější servery pro spolupráci s touto službou. A pro úplnost jsou uvedena schémata používaných XML souborů.
|
|
|
Automata in Infinite-state Formal Verification
Lengál, Ondřej ; Jančar, Petr (oponent) ; Veith, Helmut (oponent) ; Esparza, Javier (oponent) ; Vojnar, Tomáš (vedoucí práce)
The work presented in this thesis focuses on finite state automata over finite words and finite trees, and the use of such automata in formal verification of infinite-state systems. First, we focus on extensions of a previously introduced framework for verifi cation of heap-manipulating programs-in particular programs with complex dynamic data structures-based on tree automata. We propose several extensions to the framework, such as making it fully automated or extending it to consider ordering over data values. Further, we also propose novel decision procedures for two logics that are often used in formal verification: separation logic and weak monadic second order logic of one successor. These decision procedures are based on a translation of the problem into the domain of automata and subsequent manipulation in the target domain. Finally, we have also developed new approaches for efficient manipulation with tree automata, mainly for testing language inclusion and for handling automata with large alphabets, and implemented them in a library for general use. The developed algorithms are used as the key technology to make the above mentioned techniques feasible in practice.
|
|
|
Poloautomatická diagnostika síťových protokolů
Svoboda, Ondřej ; Ryšavý, Ondřej (oponent) ; Holkovič, Martin (vedoucí práce)
Tato práce se zabývá poloautomatickou diagnostikou síťových protokolů. Řeší se zde, jak z příkladů komunikace sestavit obecný popis protokolů. Nejprve jsou představeny různé techniky odposlechu síťového provozu spolu s programy, které se často k odchytávání komunikace používají. Také budou popsány některé známé síťové protokoly se zaměřením na jejich komunikační zprávy. V další části budou popsány již existující metody získávání popisu z příkladů a definovány vlastnosti těchto metod. Následuje návrh architektury vyvíjeného nástroje společně s návrhem metod tvorby popisu protokolu. Další část se věnuje implementaci vytvářeného nástroje a na závěr je tento nástroj otestován a jsou s ním prováděny experimenty.
|
|
|
Generátor konečných automatů z grafického popisu pro jazyk VHDL
Janyš, Martin ; Košař, Vlastimil (oponent) ; Šimek, Václav (vedoucí práce)
Práce seznamuje čtenáře s možnostmi návrhu a tvorby konečných stavových automatů s důrazem na reprezentaci pomocí jazyka VHDL. Hlavním tématem je aplikace, která implementuje generátor VHDL kódu na základě gra fického popisu, který je možné v něm vytvořit. Popsány jsou klíčové oblasti aplikace. Zejména jejich použití a implementace, která realizuje samotný převod stavového diagramu do VHDL.
|
|
|
Kontextem řízený lexikální analyzátor
Hatina, Peter ; Koutný, Jiří (oponent) ; Čermák, Martin (vedoucí práce)
Tato práce se věnuje základním principům lexikální analýzy a způsobu kontextového rozpoznání typu lexému v závislosti na jeho pozici ve zdrojovém souboru. V práci bude popsán princip lexikální analýzy, postup tvorby lexikálního analyzátoru a možné řešení kontextového rozlišení lexémů, založené na automatovém systému. Lexikální analyzátor je rozšířen o vlastnost rozpoznávat tokeny v blocích kódu dalších jazyků.
|
|
|
Implementace obecného zpětného assembleru
Přikryl, Zdeněk ; Masařík, Karel (oponent) ; Lukáš, Roman (vedoucí práce)
Tato práce popisuje proces vytváření disassembleru pro nově navrhované procesory. Kritériem při vytváření je jeho automatické vygenerování. Instrukční sada pro procesor je modelována pomocí specializovaného jazyka ISAC, který obsluhuje prostředky pro popis této instrukční sady, jako je například formát instrukce v jazyku symbolických instrukcí, binární zápis instrukce a chování instrukce. Vnitřním modelem je párový konečný automat, který formálně popíše vztah mezi textovou reprezentací instrukce a binárním kódováním instrukce. Z tohoto vnitřního modelu je generován kód překladače - disassembleru. Ten na vstupu přijímá program ve strojovém kódu a generuje ekvivalentní program v jazyce symbolických instrukcí.
|
|
|
Simulace a protiřetězce pro efektivní práci s konečnými automaty
Holík, Lukáš ; Černá, Ivana (oponent) ; Jančar, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis is focused on techniques for finite automata and their use in practice, with the main emphasis on nondeterministic tree automata. This concerns namely techniques for size reduction and language inclusion testing, which are two problems that are crucial for many applications of tree automata. For size reduction of tree automata, we adapt the simulation quotient technique that is well established for finite word automata. We give efficient algorithms for computing tree automata simulations and we also introduce a new type of relation that arises from a combination of tree automata downward and upward simulation and that is very well suited for quotienting. The combination principle is relevant also for word automata. We then generalise the so called antichain universality and language inclusion checking technique developed originally for finite word automata for tree automata. Subsequently, we improve the antichain technique for both word and tree automata by combining it with the simulation-based inclusion checking techniques, significantly improving efficiency of the antichain method. We then show how the developed reduction and inclusion checking methods improve the method of abstract regular tree model checking, the method that was the original motivation for starting the work on tree automata. Both the reduction and the language inclusion methods are based on relatively simple and general principles that can be further extended for other types of automata and related formalisms. An example is our adaptation of the reduction methods for alternating Büchi automata, which results in an efficient alternating automata size reduction technique.
|
|
|
Syntaktická analýza založená na párových automatech
Zámečníková, Eva ; Masařík, Karel (oponent) ; Lukáš, Roman (vedoucí práce)
Diplomová práce pojednává o syntaktické analýze založené na modelu párových automatů. Konečný párový automat obsahuje vstupní a výstupní automat. Vstupní automat provádí syntaktickou analýzu se vstupním řetězcem. Použitá pravidla vstupního automatu řídí výstupní automat, který generuje výstupní řetězec. V práci je popsán způsob determinizace vstupního automatu bez ztráty informací o pravidlech použitých v původním automatu. Determinizace je rozdělena na dvě části - pro převodníky specifikující konečný a nekonečný překlad. Dále je prezentován párový automat se zvýšenou výpočetní silou. Zvýšení síly spočívá v nahrazení vstupního či výstupního automatu nebo jen jeho části bezkontextovou gramatikou.
|
|
|
An Automata-Based Decision Procedure
Hečko, Michal ; Češka, Milan (oponent) ; Lengál, Ondřej (vedoucí práce)
Presburger arithmetics (PrA) is a decidable, first-order theory of natural numbers, with applications in many areas in formal verification of software properties. SMT-solvers tools implementing various algorithmic approaches to deciding whether a formula has a solution play a crucial role in formal verification. In this work, we document building a novel automatic SMT solver for PrA based on finite automata an approach that no SMT solver currently employs. We provide an overview of challenges and their solutions arising from the complexity of such a tool, including results from the conducted experiments already showing problems in which this alternative approach outperforms the state-of-the-art solvers. We have also identified problems in which the performance of the automata-based procedure struggles, which are open research opportunities.
|
|
|
Hardwarová akcelerace útoku na šifrování
Okuliar, Adam ; Slaný, Karel (oponent) ; Vašíček, Zdeněk (vedoucí práce)
Hardwarová akcelerácia výpočtu býva často vhodným nástrojom ako docieliť výrazne lepšieho výkonu pri spracovávaní veľkého množstva dát alebo pri realizácii algoritmu ktorý je možné dobre paralelizovať. Cieľom práce je demonštrovať výsledky použitia FPGA obvodov na implementáciu algoritmu s exponenciálnou zložitosťou. Zvoleným algoritmom je útok hrubou silou na šifrovací algoritmus WEP so 40 bitovým klúčom. Účelom práce je porovnať vlastnosti a výkon softwarovej a hardwarovej implementácie algoritmu.
|
host ::
RSS.