|
STRAIN ENGINEERING OF THE ELECTRONIC STRUCTURE OF 2D MATERIALS
del Corro, Elena ; Peňa-Alvarez, M. ; Morales-García, A. ; Bouša, Milan ; Řáhová, Jaroslava ; Kavan, Ladislav ; Kalbáč, Martin ; Frank, Otakar
The research on graphene has attracted much attention since its first successful preparation in 2004. It possesses many unique properties, such as an extreme stiffness and strength, high electron mobility, ballistic transport even at room temperature, superior thermal conductivity and many others. The affection for graphene was followed swiftly by a keen interest in other two dimensional materials like transition metal dichalcogenides. As has been predicted and in part proven experimentally, the electronic properties of these materials can be modified by various means. The most common ones include covalent or non-covalent chemistry, electrochemical, gate or atomic doping, or quantum confinement. None of these methods has proven universal enough in terms of the devices' characteristics or scalability. However, another approach is known mechanical strain/stress, but experiments in that direction are scarce, in spite of their high promises.\nThe primary challenge consists in the understanding of the mechanical properties of 2D materials and in the ability to quantify the lattice deformation. Several techniques can be then used to apply strain to the specimens and thus to induce changes in their electronic structure. We will review their basic concepts and some of the examples so far documented experimentally and/or theoretically.
|
|
Modelling, parameter estimation, optimisation and control of transport and reaction processes in bioreactors.
ŠTUMBAUER, Václav
With the significant potential of microalgae as a major biofuel source of the future, a considerable scientific attention is attracted towards the field of biotechnology and bioprocess engineering. Nevertheless the current photobioreactor (PBR) design methods are still too empirical. With this work I would like to promote the idea of designing a production system, such as a PBR, completely \emph{in silico}, thus allowing for the in silico optimization and optimal control determination. The thesis deals with the PBR modeling and simulation. It addresses two crucial issues in the current state-of-the-art PBR modeling. The first issue relevant to the deficiency of the currently available models - the incorrect or insufficient treatment of either the transport process modeling, the reaction modeling or the coupling between these two models. A correct treatment of both the transport and the reaction phenomena is proposed in the thesis - in the form of a unified modeling framework consisting of three interconnected parts - (i) the state system, (ii) the fluid-dynamic model and (iii) optimal control determination. The proposed model structure allows prediction of the PBR performance with respect to the modelled PBR size, geometry, operating conditions or a particular microalgae strain. The proposed unified modeling approach is applied to the case of the Couette-Taylor photobioreactor (CTBR) where it is used for the optimal control solution. The PBR represents a complex multiscale problem and especially in the case of the production scale systems, the associated computational costs are paramount. This is the second crucial issue addressed in the thesis. With respect to the computational complexity, the fluid dynamics simulation is the most costly part of the PBR simulation. To model the fluid flow with the classical CFD (Computational Fluid Dynamics) methods inside a production scale PBR leads to an enormous grid size. This usually requires a parallel implementation of the solver but in the parallelization of the classical methods lies another relevant issue - that of the amount of data the individual nodes must interchange with each other. The thesis addresses the performance relevant issues by proposing and evaluation alternative approaches to the fluid flow simulation. These approaches are more suitable to the parallel implementation than the classical methods because of their rather local character in comparison to the classical methods - namely the Lattice Boltzmann Method (LBM) for fluid flow, which is the primary focus of the thesis in this regard and alternatively also the discrete random walk based method (DRW). As the outcome of the thesis I have developed and validated a new Lagrangian general modeling approach to the transport and reaction processes in PBR - a framework based on the Lattice Boltzmann method (LBM) and the model of the Photosynthetic Factory (PSF) that models correctly the transport and reaction processes and their coupling. Further I have implemented a software prototype based on the proposed modeling approach and validated this prototype on the case of the Coutte-Taylor PBR. I have also demonstrated that the modeling approach has a significant potential from the computational costs point of view by implementing and validating the software prototype on the parallel architecture of CUDA (Compute Unified Device Architecture). The current parallel implementation is approximately 20 times faster than the unparallized one and decreases thus significantly the iteration cycle of the PBR design process.
|
|
Effect of snowpack on runoff generation during rain on snow event.
Juras, Roman ; Máca, Petr (advisor) ; Ladislav , Ladislav (referee)
During a winter season, when snow covers the watershed, the frequency of rain-on-snow (ROS) events is still raising. ROS can cause severe natural hazards like floods or wet avalanches. Prediction of ROS effects is linked to better understanding of snowpack runoff dynamics and its composition. Deploying rainfall simulation together with hydrological tracers was tested as a convenient tool for this purpose. Overall 18 sprinkling experiments were conducted on snow featuring different initial conditions in mountainous regions over middle and western Europe.
Dye tracer brilliant blue (FCF) was used for flow regime determination, because it enables to visualise preferential paths and layers interface. Snowpack runoff composition was assessed by hydrograph separation method, which provided appropriate results with acceptable uncertainty. It was not possible to use concurrently these two techniques because of technical reasons, however it would extend our gained knowledge. Snowmelt water amount in the snowpack runoff was estimated by energy balance (EB) equation, which is very efficient but quality inputs demanding. This was also the reason, why EB was deployed within only single experiment.
Timing of snowpack runoff onset decrease mainly with the rain intensity. Initial snowpack properties like bulk density or wetness are less important for time of runoff generation compared to the rain intensity. On the other het when same rain intensity was applied, non-ripe snowpack featuring less bulk density created runoff faster than the ripe snowpack featuring higher bulk density. Snowpack runoff magnitude mainly depends on the snowpack initial saturation. Ripe snowpack with higher saturation enabled to generate higher cumulative runoff where contributed by max 50 %. In contrary, rainwater travelled through the non-ripe snowpack relatively fast and contributed runoff by approx. 80 %.
Runoff prediction was tested by deploying Richards equation included in SNOWPACK model. The model was modified using a dual-domain approach to better simulate snowpack runoff under preferential flow conditions. Presented approach demonstrated an improvement in all simulated aspects compared to the more traditional method when only matrix flow is considered.
|
|
Design of Experiment for Non-Stationary Processes of Production
Jadrná, Monika ; Macák, Tomáš (advisor)
The doctoral thesis is concerned with the services sector and the area of mass production. Particularly, the optimization of the product portfolio of the travel agency and the optimization of production rounds of ammunition.
The theoretical part deals with the current overview of discussed topic. Further, the terminology and methods of the decision-making process are defined to support decision making. The theoretical basis of research focused on the choice of appropriate input variables in the area of services, and on the choice of a particular material option in the production area and appropriate equipment for the production. The theoretical part forms the basis for the practical part of the thesis.
For the doctoral thesis was chosen an enterprise operating in the defined sector. Product portfolio for the services sector is optimised using Fuzzy logic and Fuzzy sets so that the enterprise can maintain its competitiveness in todays highly ambitious market. Product portfolio for manufacture is optimised for achieving desired properties of the product.
The main aim of the thesis is to propose a new methodological approach for the management of selected business processes in their nonstationary time course. The aim of the practical implementation is to verify the functionality of the proposed methodological approach, both in the area of services and in the field of mass production.
|
|
New Methods for Increasing Efficiency and Speed of Functional Verification
Zachariášová, Marcela ; Dohnal, Jan (referee) ; Steininger, Andreas (referee) ; Kotásek, Zdeněk (advisor)
Při vývoji současných číslicových systémů, např. vestavěných systému a počítačového hardware, je nutné hledat postupy, jak zvýšit jejich spolehlivost. Jednou z možností je zvyšování efektivity a rychlosti verifikačních procesů, které se provádějí v raných fázích návrhu. V této dizertační práci se pozornost věnuje verifikačnímu přístupu s názvem funkční verifikace. Je identifikováno několik výzev a problému týkajících se efektivity a rychlosti funkční verifikace a ty jsou následně řešeny v cílech dizertační práce. První cíl se zaměřuje na redukci simulačního času v průběhu verifikace komplexních systémů. Důvodem je, že simulace inherentně paralelního hardwarového systému trvá velmi dlouho v porovnání s během v skutečném hardware. Je proto navrhnuta optimalizační technika, která umisťuje verifikovaný systém do FPGA akcelerátoru, zatím co část verifikačního prostředí stále běží v simulaci. Tímto přemístěním je možné výrazně zredukovat simulační režii. Druhý cíl se zabývá ručně připravovanými verifikačními prostředími, která představují výrazné omezení ve verifikační produktivitě. Tato režie však není nutná, protože většina verifikačních prostředí má velice podobnou strukturu, jelikož využívají komponenty standardních verifikačních metodik. Tyto komponenty se jen upravují s ohledem na verifikovaný systém. Proto druhá optimalizační technika analyzuje popis systému na vyšší úrovni abstrakce a automatizuje tvorbu verifikačních prostředí tím, že je automaticky generuje z tohoto vysoko-úrovňového popisu. Třetí cíl zkoumá, jak je možné docílit úplnost verifikace pomocí inteligentní automatizace. Úplnost verifikace se typicky měří pomocí různých metrik pokrytí a verifikace je ukončena, když je dosažena právě vysoká úroveň pokrytí. Proto je navržena třetí optimalizační technika, která řídí generování vstupů pro verifikovaný systém tak, aby tyto vstupy aktivovali současně co nejvíc bodů pokrytí a aby byla rychlost konvergence k maximálnímu pokrytí co nejvyšší. Jako hlavní optimalizační prostředek se používá genetický algoritmus, který je přizpůsoben pro funkční verifikaci a jeho parametry jsou vyladěny pro tuto doménu. Běží na pozadí verifikačního procesu, analyzuje dosažené pokrytí a na základě toho dynamicky upravuje omezující podmínky pro generátor vstupů. Tyto podmínky jsou reprezentovány pravděpodobnostmi, které určují výběr vhodných hodnot ze vstupní domény. Čtvrtý cíl diskutuje, zda je možné znovu použít vstupy z funkční verifikace pro účely regresního testování a optimalizovat je tak, aby byla rychlost testování co nejvyšší. Ve funkční verifikaci je totiž běžné, že vstupy jsou značně redundantní, jelikož jsou produkovány generátorem. Pro regresní testy ale tato redundance není potřebná a proto může být eliminována. Zároveň je ale nutné dbát na to, aby úroveň pokrytí dosáhnutá optimalizovanou sadou byla stejná, jako u té původní. Čtvrtá optimalizační technika toto reflektuje a opět používá genetický algoritmus jako optimalizační prostředek. Tentokrát ale není integrován do procesu verifikace, ale je použit až po její ukončení. Velmi rychle odstraňuje redundanci z původní sady vstupů a výsledná doba simulace je tak značně optimalizována.
|
|
Packet Classification Algorithms
Puš, Viktor ; Lhotka,, Ladislav (referee) ; Dvořák, Václav (advisor)
Tato práce se zabývá klasifikací paketů v počítačových sítích. Klasifikace paketů je klíčovou úlohou mnoha síťových zařízení, především paketových filtrů - firewallů. Práce se tedy týká oblasti počítačové bezpečnosti. Práce je zaměřena na vysokorychlostní sítě s přenosovou rychlostí 100 Gb/s a více. V těchto případech nelze použít pro klasifikaci obecné procesory, které svým výkonem zdaleka nevyhovují požadavkům na rychlost. Proto se využívají specializované technické prostředky, především obvody ASIC a FPGA. Neméně důležitý je také samotný algoritmus klasifikace. Existuje mnoho algoritmů klasifikace paketů předpokládajících hardwarovou implementaci, přesto však tyto přístupy nejsou připraveny pro velmi rychlé sítě. Dizertační práce se proto zabývá návrhem nových algoritmů klasifikace paketů se zaměřením na vysokorychlostní implementaci ve specializovaném hardware. Je navržen algoritmus, který dělí problém klasifikace na jednodušší podproblémy. Prvním krokem je operace vyhledání nejdelšího shodného prefixu, používaná také při směrování paketů v IP sítích. Tato práce předpokládá využití některého existujícího přístupu, neboť již byly prezentovány algoritmy s dostatečnou rychlostí. Následujícím krokem je mapování nalezených prefixů na číslo pravidla. V této části práce přináší vylepšení využitím na míru vytvořené hashovací funkce. Díky použití hashovací funkce lze mapování provést v konstantním čase a využít při tom pouze jednu paměť s úzkým datovým rozhraním. Rychlost tohoto algoritmu lze určit analyticky a nezávisí na počtu pravidel ani na charakteru síťového provozu. S využitím dostupných součástek lze dosáhnout propustnosti 266 milionů paketů za sekundu. Následující tři algoritmy uvedené v této práci snižují paměťové nároky prvního algoritmu, aniž by ovlivňovaly rychlost. Druhý algoritmus snižuje velikost paměti o 11 % až 96 % v závislosti na sadě pravidel. Nevýhodu nízké stability odstraňuje třetí algoritmus, který v porovnání s prvním zmenšuje paměťové nároky o 31 % až 84 %. Čtvrtý algoritmus kombinuje třetí algoritmus se starším přístupem a díky využití několika technik zmenšuje paměťové nároky o 73 % až 99 %.
|
|
Harnessing Forest Automata for Verification of Heap Manipulating Programs
Šimáček, Jiří ; Abdulla, Parosh (referee) ; Křetínský, Mojmír (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zabývá verifikací nekonečně stavových systémů, konkrétně, verifikací programů využívajích složité dynamicky propojované datové struktury. V minulosti se k řešení tohoto problému objevilo mnoho různých přístupů, avšak žádný z nich doposud nebyl natolik robustní, aby fungoval ve všech případech, se kterými se lze v praxi setkat. Ve snaze poskytnout vyšší úroveň automatizace a současně umožnit verifikaci programů se složitějšími datovými strukturami v této práci navrhujeme nový přístup, který je založen zejména na použití stromových automatů, ale je také částečně inspirován některými myšlenkami, které jsou převzaty z metod založených na separační logice. Mimo to také představujeme několik vylepšení v oblasti implementace operací nad stromovými automaty, které jsou klíčové pro praktickou využitelnost navrhované verifikační metody. Konkrétně uvádíme optimalizovaný algoritmus pro výpočet simulací pro přechodový systém s návěštími, pomocí kterého lze efektivněji počítat simulace pro stromové automaty. Dále uvádíme nový algoritmus pro testování inkluze stromových automatů společně s experimenty, které ukazují, že tento algoritmus překonává jiné existující přístupy.
|
|
Acceleration of Object Detection Using Classifiers
Juránek, Roman ; Kälviäinen, Heikki (referee) ; Sojka, Eduard (referee) ; Zemčík, Pavel (advisor)
Detekce objektů v počítačovém vidění je složítá úloha. Velmi populární a rozšířená metoda pro detekci je využití statistických klasifikátorů a skenovacích oken. Pro učení kalsifikátorů se často používá algoritmus AdaBoost (nebo jeho modifikace), protože dosahuje vysoké úspěšnosti detekce, nízkého počtu chybných detekcí a je vhodný pro detekci v reálném čase. Implementaci detekce objektů je možné provést různými způsoby a lze využít vlastnosti konkrétní architektury, pro urychlení detekce. Pro akceleraci je možné využít grafické procesory, vícejádrové architektury, SIMD instrukce, nebo programovatelný hardware. Tato práce představuje metodu optimalizace, která vylepšuje výkon detekce objektů s ohledem na cenovou funkci zadanou uživatelem. Metoda rozděluje předem natrénovaný klasifikátor do několika různých implementací, tak aby celková cena klasifikace byla minimalizována. Metoda je verifikována na základním experimentu, kdy je klasifikátor rozdělen do předzpracovací jednotku v FPGA a do jednotky ve standardním PC.
|
|
Analysis and Testing of Concurrent Programs
Letko, Zdeněk ; Lourenco, Joao (referee) ; Sekanina, Lukáš (referee) ; Vojnar, Tomáš (advisor)
V disertační práci je nejprve uvedena taxonomie chyb v souběžném zpracování dat a přehled technik pro jejich dynamickou detekci. Následně jsou navrženy nové metriky pro měření synchronizace a souběžného chování programů společně s metodologií jejich odvozování. Tyto techniky se zejména uplatní v testování využívajícím techniky prohledávání prostoru a v saturačním testování. Práce dále představuje novou heuristiku vkládání šumu, jejímž cílem je maximalizace proložení instrukcí pozorovaných během testování. Tato heuristika je porovnána s již existujícími heuristikami na několika testech. Výsledky ukazují, že nová heuristika překonává ty existující v určitých případech. Nakonec práce představuje inovativní aplikaci stochastických optimalizačních algoritmů v procesu testování vícevláknových aplikací. Principem metody je hledání vhodných kombinací parametrů testů a metod vkládání šumu. Tato metoda byla prototypově implementována a otestována na množině testovacích příkladů. Výsledky ukazují, že metoda má potenciál vyznamně vylepšit testování vícevláknových programů.
|
|
Relational Verification of Programs with Integer Data
Konečný, Filip ; Bouajjani, Ahmed (referee) ; Jančar, Petr (referee) ; Vojnar, Tomáš (advisor)
Tato práce představuje nové metody pro verifikaci programů pracujících s neomezenými celočíslenými proměnnými, konkrétně metody pro analýzu dosažitelnosti a~konečnosti. Většina těchto metod je založena na akceleračních technikách, které počítají tranzitivní uzávěry cyklů programu. V práci je nejprve představen algoritmus pro akceleraci několika tříd celočíselných relací. Tento algoritmus je až o čtyři řády rychlejší než existující techniky. Z teoretického hlediska práce dokazuje, že uvažované třídy relací jsou periodické a~poskytuje tudíž jednotné řešení prolému akcelerace. Práce dále představuje semi-algoritmus pro analýzu dosažitelnosti celočíselných programů, který sleduje relace mezi proměnnými programu a~aplikuje akcelerační techniky za účelem modulárního výpočtu souhrnů procedur. Dále je v práci navržen alternativní algoritmus pro analýzu dosažitelnosti, který integruje predikátovou abstrakci s accelerací s cílem zvýšit pravděpodobnost konvergence výpočtu. Provedené experimenty ukazují, že oba algoritmy lze úspěšně aplikovat k verifikaci programů, na kterých předchozí metody selhávaly. Práce se rovněž zabývá problémem konečnosti běhu programů a~dokazuje, že tento problém je rozhodnutelný pro několik tříd celočíselných relací. Pro některé z těchto tříd relací je v práci navržen algoritmus, který v polynomiálním čase vypočítá množinu všech konfigurací programu, z nichž existuje nekonečný běh. Tento algoritmus je integrován do metody, která analyzuje konečnost běhů celočíselných programů. Efektivnost této metody je demonstrována na několika netriviálních celočíselných programech.
|
guest ::
