|
|
Porovnání konvenčních PTP a PTN s proudovými a napěťovými senzory
Dvořák, Petr ; Drápela, Jiří (oponent) ; Orságová, Jaroslava (vedoucí práce)
Diplomová práce se zabývá konvenčními přístrojovými transformátory a proudovými a napěťovými senzory. První polovina práce popisuje zejména základní pojmy a třídy přesnosti těchto převodníků používaných v elektrických rozvodnách. Důraz je kladen především na vzájemné rozdíly. Ve druhé polovině práce je uveden přesný typ převodníků, které jsou instalovány v rozvodně Medlánky. Z dlouhodobého monitoringu z této rozvodny je provedena analýza naměřených dat a porovnání výsledků z klasických přístrojových transformátorů oproti výsledkům z modernějších senzorů.
|
|
|
Nástroj pro abstraktní regulární model checking
Chalk, Matěj ; Rogalewicz, Adam (oponent) ; Hruška, Martin (vedoucí práce)
Metody formální verifikace mohou poskytnout automatizované ověření korektnosti softwaru (stavěné na matematických základech), což je velmi důležité. Jednou z těchto metod je abstraktní regulární model checking, jenž používá konečné automaty a převodníky pro reprezentaci množiny dosažitelných konfigurací, respektive jednokrokového přechodu mezi těmito konfiguracemi. Přestože tato metoda řeší obecně nerozhodnutelné problémy, umožňuje terminaci v mnoha praktických případech a navíc výrazně zmírňuje problém stavové exploze. Tohoto dosahuje urychlením výpočtu dosažitelných stavů pomocí inkrementálního zjemňování abstrakcí, k odstranění neplatných protipříkladů vzniklých nadaproximací pak slouží technika zjemňování abstrakce založená na protipříkladech. Cílem této práce je vytvořit dobře navržený nástroj pro abstraktní regulární model checking, jenž byl dosud implementován pouze v prototypech. Nový nástroj bude systémy modelovat pomocí symbolických automatů a převodníků namísto jejich (méně stručných) klasických alternativ.
|
|
|
Synchronous Formal Systems Based on Grammars and Transducers
Horáček, Petr ; Janoušek, Jan (oponent) ; Yamamura,, Akihito (oponent) ; Meduna, Alexandr (vedoucí práce)
This doctoral thesis studies synchronous formal systems based on grammars and transducers, investigating both theoretical properties and practical application perspectives. It introduces new concepts and definitions building upon the well-known principles of regulated rewriting and synchronization. An alternate approach to synchronization of context-free grammars is proposed, based on linked rules. This principle is extended to regulated grammars such as scattered context grammars and matrix grammars. Moreover, based on a similar principle, a new type of transducer called the rule-restricted transducer is introduced as a system consisting of a finite automaton and context-free grammar. New theoretical results regarding the generative and accepting power are presented. The last part of the thesis studies linguistically-oriented application perspectives, focusing on natural language translation. The main advantages of the new models are discussed and compared, using select case studies from Czech, English, and Japanese to illustrate.
|
|
|
Klasifikace ve stavebnictví, jejich vývoj a použití
Vydrová, Michaela ; Dvořák, Jiří (oponent) ; Nový, Martin (vedoucí práce)
Teoretická část bakalářské práce se zabývá významem třídění ve stavební výrobě. Popisuje historický vývoj a význam klasifikací ve stavebnictví. Sleduje použití klasifikací a třídníků v praxi a využití v české legislativě. Praktická část se zabývá příklady zatřídění konkrétních stavebních objektů a stavebních prací. Část práce se zabývá zjištěním ceny rodinného domu v jiném období, než byla plánovaná výstavba.
|
|
|
Systémy převodníků
Skácel, Jiří ; Kučera, Jiří (oponent) ; Meduna, Alexandr (vedoucí práce)
Tato práce zavádí systémy zásobníkových převodníků. Základní myšlenka vychází z kooperujících distribuovaných gramatických systémů, které umožňují práci více gramatik na jednom řetězci. Převodníky spolupracují předáváním výsledků svých překladů jako vstupu pro další komponentu. Dále tato práce zkoumá jejich popisnou sílu a ekvivalenci systémů s různými počty komponent. Hlavním závěrem je pak porovnání popisné síly s Turingovými stroji a to s ohledem na jimi definovaný překlad i přijímané jazyky.
|
|
|
Improvements of the ASMA Tool for Analysis of String Manipulating Programs via Symbolic Automata
Kmenta, Martin ; Lengál, Ondřej (oponent) ; Vojnar, Tomáš (vedoucí práce)
In this work we deal with regular model checking which is a technique for analyzing programs whose state space can be infinite due to dealing with, e.g. unbounded queues, parameters, dynamically linked data structures, recursive procedures, or strings. The goal of this work was to implement improvements to the existing prototype tool ASMA implementing regular model checking over the Microsoft Automata library. We analysed the source code of ASMA and reran analyses of all available benchmark programs. We identified some bottlenecks and have tackled several of them. In particular, we integrated a library containing additional reduction algorithms into ASMA, created several new versions of the reverse concatenation operation, which tuned out to be very costly in the benchmarks, improved the command line interface of ASMA, and implemented some other optimizations for ASMA. The computation time was reduced by 90 % when analysing bigger programs.
|
|
|
Data Acquisition and Control System of Hydroelectric Power Plant Using Internet Techniques
Sattouf, Mousa ; Přikryl, Hynek (oponent) ; Richter, Aleš (oponent) ; Skalický, Jiří (vedoucí práce)
Hydropower has now become the best source of electricity on earth. It is produced due to the energy provided by moving or falling water. History proves that the cost of this electricity remains constant over the year. Because of the many advantages, most of the countries now have hydropower as the source of major electricity producer. The most important advantage of hydropower is that it is green energy, which mean that no air or water pollutants are produced, also no greenhouse gases like carbon dioxide are produced which makes this source of energy environment-friendly. It prevents us from the danger of global warming. Using internet techniques to control several hydroelectric plants has very important advantages, as reducing operating costs and the flexibility of meeting changes of energy demand occurred in consumption side. Also it is very effective to confront large disturbances of electrical grid, such as adding or removing large loads, and faults. In the other hand, data acquisition systems provides very useful information for both typical and scientific analysis, such as economical costs reducing, fault prediction systems, demand prediction, maintenance schedules, decision support systems and many other benefits. This thesis describes a generalized model which can be used to simulate a data acquisition and control system of hydroelectric power plant using MATLAB/SIMULINK and TrueTime simulink library. The plant considered consists of hydro turbine connected to synchronous generator with excitation system, and the generator is connected to public grid. Simulation of hydro turbine and synchronous generator can be done using various simulation tools, In this work, SIMULINK/MATLAB is favored over other tools in modeling the dynamics of a hydro turbine and synchronous machine. The SIMULINK program in MATLAB is used to obtain a schematic model of the hydro plant by means of basic function blocks. This approach is pedagogically better than using a compilation of program code as in other software programs .The library of SIMULINK software programs includes function blocks which can be linked and edited to model. Either Simulink Real-Time library or TrueTime library can be used to build and simulate internet and real time systems, in this thesis the TrueTime library was used.
|
|
|
Improvements of the ASMA Tool for Analysis of String Manipulating Programs via Symbolic Automata
Kmenta, Martin ; Lengál, Ondřej (oponent) ; Vojnar, Tomáš (vedoucí práce)
In this work we deal with regular model checking which is a technique for analyzing programs whose state space can be infinite due to dealing with, e.g. unbounded queues, parameters, dynamically linked data structures, recursive procedures, or strings. The goal of this work was to implement improvements to the existing prototype tool ASMA implementing regular model checking over the Microsoft Automata library. We analysed the source code of ASMA and reran analyses of all available benchmark programs. We identified some bottlenecks and have tackled several of them. In particular, we integrated a library containing additional reduction algorithms into ASMA, created several new versions of the reverse concatenation operation, which tuned out to be very costly in the benchmarks, improved the command line interface of ASMA, and implemented some other optimizations for ASMA. The computation time was reduced by 90 % when analysing bigger programs.
|
|
|
Porovnání konvenčních PTP a PTN s proudovými a napěťovými senzory
Dvořák, Petr ; Drápela, Jiří (oponent) ; Orságová, Jaroslava (vedoucí práce)
Diplomová práce se zabývá konvenčními přístrojovými transformátory a proudovými a napěťovými senzory. První polovina práce popisuje zejména základní pojmy a třídy přesnosti těchto převodníků používaných v elektrických rozvodnách. Důraz je kladen především na vzájemné rozdíly. Ve druhé polovině práce je uveden přesný typ převodníků, které jsou instalovány v rozvodně Medlánky. Z dlouhodobého monitoringu z této rozvodny je provedena analýza naměřených dat a porovnání výsledků z klasických přístrojových transformátorů oproti výsledkům z modernějších senzorů.
|
|
|
Nástroj pro abstraktní regulární model checking
Chalk, Matěj ; Rogalewicz, Adam (oponent) ; Hruška, Martin (vedoucí práce)
Metody formální verifikace mohou poskytnout automatizované ověření korektnosti softwaru (stavěné na matematických základech), což je velmi důležité. Jednou z těchto metod je abstraktní regulární model checking, jenž používá konečné automaty a převodníky pro reprezentaci množiny dosažitelných konfigurací, respektive jednokrokového přechodu mezi těmito konfiguracemi. Přestože tato metoda řeší obecně nerozhodnutelné problémy, umožňuje terminaci v mnoha praktických případech a navíc výrazně zmírňuje problém stavové exploze. Tohoto dosahuje urychlením výpočtu dosažitelných stavů pomocí inkrementálního zjemňování abstrakcí, k odstranění neplatných protipříkladů vzniklých nadaproximací pak slouží technika zjemňování abstrakce založená na protipříkladech. Cílem této práce je vytvořit dobře navržený nástroj pro abstraktní regulární model checking, jenž byl dosud implementován pouze v prototypech. Nový nástroj bude systémy modelovat pomocí symbolických automatů a převodníků namísto jejich (méně stručných) klasických alternativ.
|
host ::
RSS.