|
Model checking nekonečně stavových systémů založený na inferenci jazyků
Rozehnal, Pavel ; Křena, Bohuslav (oponent) ; Vojnar, Tomáš (vedoucí práce)
Regulární model checking je metoda pro verifikaci nekonečně stavových systémů. Je založena na kódování jejich konfigurace jako slov nad konečnou abecedou, množiny konfigurací jako konečného automatu a přechodů jako konečných transducerů. Je zde představen nový přístup k regulárnímu model checkingu založený na odvozování regulárních jazyků. Metoda je založena na prozkoumávání nekonečně stavového systému, jehož chování může být modelováno použitím transducerů, které zachovávají délku řetězců a jejich aplikací je možné získat všechny dosažitelné konfigurace systému. Naše metoda regulárního model checkingu je založena na odvozování regulárních jazyků pomocí algoritmu Angluin, který je použit pro nalezení vhodného invariantu (nadaproximace), který je schopen zodpovedět otázku zachování či porušení nějaké vlastnosti. Je zde také uveden úvod do teorie konečných automatů, model checkingu, SAT problémů a popis Angluinova a Biermanova algoritmu pro učení konečných automatů.
|
|
Docházkový a přístupový systém a jeho využití v podnikové praxi
Šimek, Jan ; Pour, Jan (vedoucí práce) ; Kreidl, Michal (oponent)
Diplomová práce se zabývá problematikou docházkových a přístupových systémů, jejich funkcí a důležitosti v podniku. Hlavním cílem je osvětlit dané téma jak IT odborníkům, tak i veřejnosti, které se snaží přiblížit úlohu vlastního systému, jeho zavedení a provoz v podnikové praxi. Práce je rozdělena do dvou hlavních částí. V první části je popsán historický vývoj sledování docházky jak z pohledu papírového a následně jeho nástupce softwarového řešení, tak i po stránce vlastního hardwaru. Dále jsou přiblíženy legislativní požadavky a omezení pro sledování pohybu zaměstnanců a záznamu docházky, kde je největším zdrojem samotný zákoník práce a úřad pro ochranu osobních údajů. Poté jsou představeny novinky současných docházkových a přístupových systémů. V druhé části je uveden samotný postup výběru a nasazení konkrétního docházkového systému, jeho konfigurace a provoz. Ten je detailně popsán v příloze diplomové práce. Důraz je kladen především na srozumitelnost a snadné pochopení probíraného tématu, jeho dopady a výhody využití. Hlavním přínosem práce je sjednocení pohledu na danou problematiku, ucelení pohledu na vlastní systém a jeho důležitou roli jako samostatného systému kooperujícího s dalšími softwarovými a hardwarovými prostředky v podniku.
|
|
Interakce mezi trhlinou a kruhovou inkluzí
Náhlík, Luboš
V příspěvku je studována interakce mezi kruhovou inkluzí a trhlinou šířící se v její blízkosti za předpokladu platnosti lineární elastické lomové mechaniky (LELM). Předpokládá se elastické chování materiálu matrice i inkluze. Jsou studovány tři případy. V prvním se trhlina nachází v určité vzdálenosti před inkluzí, ve druhém se vrchol trhliny nachází také před inkluzí, ale osa trhliny je posunuta vůči ose inkluze. Ve třetím případě se vrchol trhliny nachází právě na rozhraní mezi matricí a inkluzí. V posledně jmenovaném případě ztrácí pojem součinitel intenzity napětí (SIN) svůj význam, neboť exponent singularity napětí je rozdílný od ½. Jako rozhodující veličina pro dalším šíření trhliny do materiálu inkluze je v práci použita velikost kritického napětí. Cílem práce je nalezení řevládající konfigurace v dvoufázovém materiálu modelovaném jako kruhové částice v matrici a popsat typické chování trhliny v tomto materiálu.
|
|
Odometrický modul pro mobilní robot
Davídek, Daniel ; Burian, František (oponent) ; Jílek, Tomáš (vedoucí práce)
Hlavním cílem této práce byl návrh a zprovoznění odometrického modulu pro mobilní robot envMap. Modul zpracovává signály z enkodérů a následně vypočítává polohu a natočení robotu spolu s pravděpodobností jeho výskytu. Vypočtená data jsou spolu s časovou značkou získanou z GPS odesílána do nad-systému pomocí sériového rozhraní. K realizaci byla zvolena vývojová deska STM32F407G. Časovače desky jsou nastavitelné do funkce enkodéru, což minimalizuje možnost ztráty informace. Byly navrženy dvě desky plošných spojů: redukce k GPS pro přivedení potřebného signálu 1PPS a nasazovací deska pro STM32F4. V této práci jsou uvedeny rovnice pro výpočty odometrických informací i pravděpodobnosti výskytu. Pro výpočet pohybu robotu je zvolena rovnice uvažující pouze pohyb po rovinné ploše. Dále je popsána struktura programu pro STM32 a jeho funkčnost. Ve výsledcích je uvedeno kompletní schéma zapojení spolu s popisem obslužného programu a jednotlivých komunikačních zpráv. Závěrem práce jsou popsána a vyhodnocena měření zjišťující parametry robotu a finální odometrické měření porovnané s GPS lokalizací jako referencí.
|
| |
| |
|
Statistická fyzika frustrovaných evolučních her
Pištěk, Miroslav ; Janiš, Václav (oponent) ; Slanina, František (vedoucí práce)
1 Název práce: Statistická fyzika frustrovaných evolučních her Autor: Miroslav Pištěk Katedra: Ústav teoretické fyziky Vedoucí diplomové práce: RNDr. František Slanina, CSc. E-mail vedoucího: slanina@fzu.cz Abstract: V posledních dvou desetiletích narůstá zájem o mezioborový výzkum alokace omezených zdrojů. Zabývá se komplexními jevy jako jsou akciové trhy nebo dopravní zácpy. Menšinová hra je multiagentním modelem frustrace vznika- jící v obdobných situacích. Je analyticky rešitelná s použitím metody replik vyvinuté v rámci statistické fyziky spinových skel. Menšinovou hru jsme zobec- nili zavedením heterogenních agentů. Díky tomu výrazně poklesla frustrace průměrného agenta. Pro mnoho konfigurací jsme obdrželi dokonce hru s klad- ným součtem. To je v původní variantě Menšinové hry neuskutečnitelné. Získaný výsledek je v kvalitativní shodě s daty z reálných akciových trhů. Klíčová slova: frustrované evoluční hry, Menšinová hra, metoda replik
|
|
Ověření možností komunikačních periferií jednodeskového systému BeagleBoard.
Hladík, René ; Zuth, Daniel (oponent) ; Věchet, Stanislav (vedoucí práce)
Obsah bakalářská práce zahrnuje druhy a možnosti komunikace, jenž nabízí rozhraní jednodeskového počítače. Ověření rozsahu komunikace při použití v mobilní robotice a následné shrnutí pro daný systém. Cílem této práce bylo poskytnout uživatelům konfiguraci jednotlivých periferií při následném využití systému BeagleBoard xM Rev C. Úvodní část práce je zaměřena na definici a shrnutí jednodeskových počítačových systémů. Přehled hlavních rozdílů mezi jednodeskovými systémy. Dále konkurence a charakteristika jednodeskových počítačů od předních světových výrobců a hardwarové odlišnosti. V další části je proveden úplný rozbor a charakteristika použitého jednodeskového počítače Beagleboard xM Rev C. Praktická realizace zahrnuje nejdůležitější komunikační rozhraní, které můžeme použít v případě prototypů mobilních systémů. Realizace USB kamery, GPIO multifunkčního rozhraní, sériovou komunikaci pomocí CMUcam3 kamerového modulu a v závěru I2C komunikace pomocí GPIO s SRF08 ultrazvukovým snímačem. Demonstrace rozmanitosti systému BeagleBoard, kterou mohou využívat všichni uživatelé vestavěných systémů v mobilní robotice. Moderní mobilní robotické systémy jsou komplexem analogových a digitálních zařízení jako jsou různé druhy senzorů, snímacích prvků, kamer a ostatních. Bakalářská práce popisuje základní konfiguraci jednotlivých možností komunikace na bázi kamer, snímačů a systémových prvků.
|
|
Představení projektu icompose - integrované řízení sdruženého pohonu a duálního zdroje energie u plně elektrických vozidel
Machan, Jaroslav ; Nedoma, Pavel ; Plíhal, Jiří
Tento příspěvek přináší stručné představení výzkumného projektu iCOMPOSE financovaného 7. rámcovým programem Evropského společenství jako součást evropské Iniciativy za zelené automobily. Cílem projektu je vytvořit jednotný koncept kontrolního systému řízení spotřeby energie pro různé konfigurace pohonného systému (s jedním nebo více elektromotory a jedním či dvěma systémy skladování energie), což umožňuje zvýšit energetickou účinnost, jízdní vlastnosti, bezpečnost a pohodlí FEV. Projekt je řešen konsorciem partnerských společností a výzkumných institucí Kompetenzzentrum - Das virtuelle Fahrzeug ,Forschungsgesellschaft mbH; Univerzita v Surrey; Lotus Cars Limited; ŠKODA AUTO a.s., Flanders' Drive; Hutchinson SA, AVL List GmbH, Infineon Technologies AG; Fraunhofer- Gesellschaft zur Förderung der angewandten Forschung E.V.
|
|
Vnitřní kontrolní systém
Nováková, Lenka ; Králíček, Vladimír (vedoucí práce) ; Svatá, Vlasta (oponent) ; Müllerová, Libuše (oponent)
Disertační práce, zaměřená na vnitřní kontrolní systém (dále jen VKS) v podniku, si klade za cíl zmapovat kontrolní systém společností se zaměřením na nákupní oddělení. Zaměřila jsem se na nákupní proces, jelikož s rostoucí tendencí outsourcingu služeb a se vzrůstající provázaností podnikatelských subjektů roste riziko podvodu právě v nákupním procesu. K výzkumu byl vybrán vzorek společností z bankovního i nebankovního prostředí, kterým byl zaslán dotazník se zaměřením na funkčnost VKS v organizaci. Bankovní instituce jsem zvolila především kvůli přísnému dohledu ze strany České národní banky (dále jen ČNB) a povinnosti pravidelného reportingu o outsourcovaných činnostech orgánu dohledu, tedy ČNB. Pojem VKS je velmi těžké jasně definovat. Hlavním důvodem je, že se v literatuře často neshoduje vymezení definice pojmu VKS, a ani jasné vymezení nástrojů, procesů a postupů. V České republice je definice VKS zmíněna také v právních předpisech, a je potřeba ji vnímat ve velmi obecné rovině. Schiffer (2009) popisuje VKS v obecné rovině jako soustavu provozních, finančních, personálních, evidenčních a ostatních kontrol, které jsou vytvořeny vedením podniku s cílem správného efektivního řízení, dodržování vnitřních pravidel, ochrany majetku a co nejpřesnější a nejpreciznější evidence postupů ve společnosti. Dvořáček (2003) píše, že na VKS je možné nahlížet jako na souhrn vzájemně propojených nástrojů, opatření, postupů a kontrolních mechanismů. V České republice obsahuje definici VKS například zákon č. 320/2001 Sb., o finanční kontrole ve veřejné správě a o změně některých zákonů (zákon o finanční kontrole), ve znění pozdějších předpisů. Aby mohl být VKS definován jako správně nastavený systém, musí se jednat o uskupení souvisejících prvků a částí, které jsou shromážděny do smysluplného celku. Mezi jednotlivými prvky a částmi musí existovat spojení, které je přesně definované.
|
host ::
