|
| |
|
|
FPGA platforma podporující .NET Micro Framework
Matyáš, Jan ; Minařík, Miloš (oponent) ; Vašíček, Zdeněk (vedoucí práce)
Záměrem práce je navrhnout a vytvořit prototyp platformy určené k vývoji vestavěných systémů, která bude sestávat z mikrokontroleru s architekturou ARM Cortex-M a programovatelného hradlového pole FPGA. Cílem je na této platformě umožnit běh open-source prostředí .NET Micro Framework. Práce stanovuje specifikaci této platformy, popisuje proces její konstrukce, způsob portace .NET Micro Frameworku a zprovoznění komunikační sběrnice mezi mikrokontrolérem a obvodem FPGA. V závěru práce je představena sada demonstračních aplikací, které čtenáře seznamují se způsobem tvorby software pro tuto navrženou platformu.
|
|
|
GPU-Accelerated Synthesis of Probabilistic Programs
Marcin, Vladimír ; Matyáš, Jiří (oponent) ; Češka, Milan (vedoucí práce)
This paper examines the problem of automatic synthesis of probabilistic programs: having a finite family of candidate programs, how can one efficiently identify a program that satisfies a given specification. Even the most straightforward synthesis problems prove to be NP-hard. An improvement to this state of practice is brought by the PAYNT tool, which tackles this problem with a novel integrated technique for synthesising probabilistic programs. Even though it efficiently deals with the exponential growth of the family size, there is still a problem with the underlying state-space explosion. To solve this problem, we have implemented GPU-oriented model-checking algorithms that takes advantage of the GPU architecture and parallelise the task at a state level of a probabilistic model. The overall acceleration that we were able to achieve with this approach was, under certain conditions, close to the theoretically possible limit of the acceleration of the whole synthesis process.
|
|
|
Bezdrátové zabezpečovací zařízení
Matyáš, Jan ; Kočí, Radek (oponent) ; Hanáček, Petr (vedoucí práce)
Tato bakalářská práce se zabývá návrhem a realizací přenosného bezdrátového zabezpečovacího zařízení umožňující kontrolu hlídaného předmětu na dálku. Zařízení se skládá z řídícího modulu umožňující nastavení a informování o aktuálním stavu zařízení a měřících modulů, které s řídícím modulem komunikují bezdrátově v pásmu ISM. Zařízení je napájeno z baterií a je u něj vyžadovaná co možná nejvyšší výdrž na jedno nabití.
|
|
|
Improving Robustness of Neural Networks against Adversarial Examples
Gaňo, Martin ; Matyáš, Jiří (oponent) ; Češka, Milan (vedoucí práce)
This work discusses adversarial attacks to image classifier neural network models. Our goal is to summarize and demonstrate adversarial methods to show that they pose a serious issue in machine learning. The important contribution of this work is the implementation of a tool for training a robust model against adversarial examples. Our approach is to minimize maximization the loss function of the target model. Related work and our own experiments leads us to use Projected gradient descent as a target attack, therefore, we train against data generated by Projected gradient descent. As a result using the framework, we can achieve accuracy more than 90% against sophisticated adversarial attacks.
|
|
|
Využití přibližné ekvivalence při návrhu přibližných obvodů
Matyáš, Jiří ; Lengál, Ondřej (oponent) ; Češka, Milan (vedoucí práce)
Tato práce je zaměřena na využití formálně verifikačních technik pro návrh funkčních aproximací kombinačních obvodů. Jsou zde důkladně prostudovány existující formální přístupy pro zkoumání přibližné ekvivalence a jejich použití při vývoji aproximovaných obvodů. V rámci této práce je navržena nová metoda, která integruje vybrané formální techniky do Kartézského genetického programování. Klíčovým bodem nového přístupu je využití prohledávací strategie, která vede evoluci směrem k řešením, která lze rychleji verifikovat. Navržený algoritmus byl implementován v rámci syntézního nástroje ABC. Jeho výkonnost byla otestována na vývoji funkčních aproximací násobiček a sčítaček s šířkami vstupních operandů 32, respektive 128 bitů. Dosažené výsledky ukazují výjimečnou škálovatelnost navržené metody.
|
|
|
Optimální rozvrhovací systém pro outdoorové aktivity
Rykala, Kryštof ; Matyáš, Jiří (oponent) ; Češka, Milan (vedoucí práce)
Práce se zabývá technologiemi a přístupy pro vytvoření informačního systému, jehož součástí a motivací je automatické plánování rozvrhu aktivit. Za pomocí smíšeného celočíselného lineárního programování je definován model optimalizačního problému plánování se zdroji a omezeními. Součástí práce jsou programy klientské, serverové a plánovací části, které dohromady tvoří systém pro správu outdoorového centra s podporou automatického plánování.
|
|
|
RONJA TWISTER pomocí FPGA
Matyáš, Jan ; Kaštil, Jan (oponent) ; Vašíček, Zdeněk (vedoucí práce)
RONJA je open-source hardwarový projekt, jehož výsledkem je stejnojmenné zařízení umožňující bezdrátový přenos dat pomocí světelného paprsku. Tato práce se zabývá elektronickým modulem RONJA Twister, tvořícím rozhraní mezi metalickým Ethernetem a vlastním optickým přenosem. Cílem práce je reimplementovat modul pomocí technologie FPGA při zachování zpětné kompatibility. V rámci práce je modul navíc rozšířen o technologii Auto-Negotiation, čímž dochází k prevenci některých problémů spojených s používáním původní varianty modulu Twister.
|
|
|
Generování protipříkladů při analýze Markovových modelů
Molek, Martin ; Matyáš, Jiří (oponent) ; Češka, Milan (vedoucí práce)
Tato práce se zabývá generováním protipříkladů v kontextu verifikace pravděpodobnostních systémů. Protipříklady jsou generovány nad Markovovými modely (přesněji DTMC). Specifikace vlastností modelu jsou zadávány pomocí logiky PCTL, která je v této práci popsána. Pro generování protipříkladů byly použity dva různé algoritmy (Best-first search a Recursive Enumration Algorithm). Práce obsahuje popis implementace algoritmů do verifikačního nástroje STORM. Výsledky experimentů ukazují, že REA je schopen pracovat s modely obsahující miliony stavů.
|
|
|
Překladač jazyka VHDL pro potřeby formální verifikace
Matyáš, Jiří ; Smrčka, Aleš (oponent) ; Charvát, Lukáš (vedoucí práce)
Cílem této bakalářské práce je navrhnout a implementovat překladač, který umožňuje převod popisu hardware z jazyka VHDL do grafové reprezentace v jazyce VAM (Variable Assignment Language). Program je určen pro potřeby formální verifikace výzkumné skupiny VeriFIT Fakulty informačních technologií VUT Brno. Důvodem vypracování této práce je poskytnutí možnosti formálně verifikovat návrh hardware s využitím vysokoúrovňových návrhových jazyků, jakým je například jazyk VHDL.
|
host ::
RSS.