|
|
Oceňování ocelových konstrukcí
Charvát, Lukáš ; Ing.Jiří Sachl (oponent) ; Marková, Leonora (vedoucí práce)
Diplomová práce se zabývá oceňováním ocelových konstrukcí z pohledu investora. V dnešní době existuje celá řada ocelových konstrukcí, jejichž výroba se částečně provádí v dílně, tzv. mostárně a zbytek montáže je provedeno přímo na stavbě, na rozdíl od stavební výroby. Z toho vzniká velký problém finančního ohodnocení celkové práce, protože montážní firmy mnohdy neuvádějí podrobný rozpis prací. Cílem práce je navrhnout postup oceňování ocelových konstrukcí ve fázi zpracování dokumentace, dílenské výroby, dopravy a montáže na staveništi technologických zařízení.
|
|
|
Automated Verification in HW/SW Co-design
Charvát, Lukáš ; Kubátová, Hana (oponent) ; Řehák, Vojtěch (oponent) ; Vojnar, Tomáš (vedoucí práce)
The subject of the thesis is to design new hardware verification techniques optimized for a process of HW/SW co-design in which hardware and software are developed in parallel to speed up the development of new embedded systems. Currently, microprocessor co-design tools typically allow to verify designs by simulation and/or functional verification. However, even extensive functional verification can miss some non-trivial bugs. Therefore, formal verification has become more and more desirable in recent years. As opposed to testing and bug-hunting techniques that only aim at detecting flaws, the goal of formal verification is to rigorously prove that the system is indeed correct. Formal verification is, however, a very demanding task, and even though a lot of progress has been achieved in this area, formal verification is far from being able to fully automatically check all relevant properties of complex designs without a significant and costly human involvement in the verification process. The thesis deals with these challenges by focusing on verification techniques based on formal approaches, but possibly relaxing or limiting their precision and generality to achieve full automation. Further, the thesis also focuses on the efficiency of the proposed techniques and their ability to deliver continuous feedback about the verification process. Special attention is devoted to the development of formal methods for checking the equivalence of microprocessor designs on various levels of abstraction. Although these designs cannot be behaviorally equivalent, they are required to give mutually corresponding results when executing the same input program, which is a property difficult to achieve. As another considered topic, the thesis proposes methods for checking correctness of mechanisms preventing data and control hazards in single-pipelined implementations of microprocessors. The approaches described in this thesis has been implemented in the form of several tools which, after examining designs of multiple pipelined microprocessors, were able to deliver promising experimental results.
|
|
|
Nástroj pro automatizované testování GUI
Vacek, Lukáš ; Charvát, Lukáš (oponent) ; Smrčka, Aleš (vedoucí práce)
Testování GUI je navzdory jeho použitelnosti a rozšířenosti poměrně nově vznikající obor. Pro ověření GUI funkčnosti se používá často ručního testování. Cílem práce je vytvořit nástroj, který lze využít k otestování a ovládání GUI. Nástrojem bude knihovna pro automatizované testování GUI s využitím metody rozpoznávání objektů. Knihovna bude detekovat základní objekty GUI a manipulovat s nimi podle jejich typického chování. Detekce objektu bude založena na zpracování obrazu a pozorování grafických změn objektu při příchozích událostech od klávesnice a myši.
|
|
|
Jazyk pro popis instrukčních sad
Forejtník, Jan ; Charvát, Lukáš (oponent) ; Smrčka, Aleš (vedoucí práce)
V této práci je představen návrh jednoduchého jazyka pro popis architektury mikroprocesoru zaměřeného na popis instrukční sady. Dále je popsána implementace interpretu tohoto jazyka, který je schopen simulovat popsanou architekturu. Tato práce může zároveň sloužit jako návod k používání tohoto interpretu.
|
|
|
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.
|
|
|
Automated Verification in HW/SW Co-design
Charvát, Lukáš ; Kubátová, Hana (oponent) ; Řehák, Vojtěch (oponent) ; Vojnar, Tomáš (vedoucí práce)
The subject of the thesis is to design new hardware verification techniques optimized for a process of HW/SW co-design in which hardware and software are developed in parallel to speed up the development of new embedded systems. Currently, microprocessor co-design tools typically allow to verify designs by simulation and/or functional verification. However, even extensive functional verification can miss some non-trivial bugs. Therefore, formal verification has become more and more desirable in recent years. As opposed to testing and bug-hunting techniques that only aim at detecting flaws, the goal of formal verification is to rigorously prove that the system is indeed correct. Formal verification is, however, a very demanding task, and even though a lot of progress has been achieved in this area, formal verification is far from being able to fully automatically check all relevant properties of complex designs without a significant and costly human involvement in the verification process. The thesis deals with these challenges by focusing on verification techniques based on formal approaches, but possibly relaxing or limiting their precision and generality to achieve full automation. Further, the thesis also focuses on the efficiency of the proposed techniques and their ability to deliver continuous feedback about the verification process. Special attention is devoted to the development of formal methods for checking the equivalence of microprocessor designs on various levels of abstraction. Although these designs cannot be behaviorally equivalent, they are required to give mutually corresponding results when executing the same input program, which is a property difficult to achieve. As another considered topic, the thesis proposes methods for checking correctness of mechanisms preventing data and control hazards in single-pipelined implementations of microprocessors. The approaches described in this thesis has been implemented in the form of several tools which, after examining designs of multiple pipelined microprocessors, were able to deliver promising experimental results.
|
|
|
Implementace algoritmu pro shlukování hran grafu
Klimčíková, Iveta ; Charvát, Lukáš (oponent) ; Smrčka, Aleš (vedoucí práce)
Cílem této práce je prozkoumat možnosti rozložení grafu a shlukování hran, aby se vylepšila celková přehlednost grafu a zredukovalo se rušení. Po shrnutí dostupných nástrojů je detailněji popsána vybraná metoda, která vylepšuje zobrazení grafu bez nutnosti změny pozice uzlů. Práce popisuje implementaci knihovny v jazyce C++ a vytvoření aplikace, pomocí které je možné použít tento algoritmus na jednoduché, ale i rozsáhlejší grafy s větším počtem uzlů a hran. Výsledné grafy je možné exportovat do vektorového formátu SVG a případně zkonvertovat do bitmapového formátu PNG.
|
|
|
Automatická tvorba obsahu databáze SQL pro podporu testování
Minářová, Alice ; Charvát, Lukáš (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato práce se zabývá navržením a implementací dvojice nástrojů pro generování dat za účelem testování. První nástroj analyzuje textový výstup databáze PostgreSQL a vytváří konfigurační soubor v nově navrženém jazyce, který popisuje, jakým způsobem se má vygenerovat obsah databáze. Druhý nástroj na základě tohoto souboru generuje skript SQL dotazů naplňujících cílovou databázi. Uživatel může přizpůsobit generovaná data vlastním požadavkům modifikací konstrukcí v doménově specifickém jazyce. Tento jazyk byl navržen tak, aby byl zásah do konfiguračního souboru pro uživatele rychlý a intuitivní. Část práce se zabývá popisem práce s tímto jazykem. Nástroje byly testovány na uměle navržených databázích i na databázi reálného systému Drupal. Jejich řízení je zcela obslouženo přes příkazový řádek, jsou tedy vhodné k použití při automatizaci.
|
|
|
Jazyk pro popis instrukčních sad
Forejtník, Jan ; Charvát, Lukáš (oponent) ; Smrčka, Aleš (vedoucí práce)
V této práci je představen návrh jednoduchého jazyka pro popis architektury mikroprocesoru zaměřeného na popis instrukční sady. Dále je popsána implementace interpretu tohoto jazyka, který je schopen simulovat popsanou architekturu. Tato práce může zároveň sloužit jako návod k používání tohoto interpretu.
|
|
|
Nástroj pro automatizované testování GUI
Vacek, Lukáš ; Charvát, Lukáš (oponent) ; Smrčka, Aleš (vedoucí práce)
Testování GUI je navzdory jeho použitelnosti a rozšířenosti poměrně nově vznikající obor. Pro ověření GUI funkčnosti se používá často ručního testování. Cílem práce je vytvořit nástroj, který lze využít k otestování a ovládání GUI. Nástrojem bude knihovna pro automatizované testování GUI s využitím metody rozpoznávání objektů. Knihovna bude detekovat základní objekty GUI a manipulovat s nimi podle jejich typického chování. Detekce objektu bude založena na zpracování obrazu a pozorování grafických změn objektu při příchozích událostech od klávesnice a myši.
|
host ::
RSS.