|
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.
|
|
Acceleration Methods for Evolutionary Design of Digital Circuits
Vašíček, Zdeněk ; Miller, Julian (referee) ; Zelinka,, Ivan (referee) ; Sekanina, Lukáš (advisor)
Ačkoliv můžeme v literatuře nalézt řadu příkladů prezentujících evoluční návrh jakožto zajímavou a slibnou alternativu k tradičním návrhovým technikám používaným v oblasti číslicových obvodů, praktické nasazení je často problematické zejména v důsledku tzv. problému škálovatelnosti, který se projevuje např. tak, že evoluční algoritmus je schopen poskytovat uspokojivé výsledky pouze pro malé instance řešeného problému. Vážný problém představuje tzv. problém škálovatelnosti evaluace fitness funkce, který je markantní zejména v oblasti syntézy kombinačních obvodů, kde doba potřebná pro ohodnocení kandidátního řešení typicky roste exponenciálně se zvyšujícím se počtem primárních vstupů. Tato disertační práce se zabývá návrhem několika metod umožňujících redukovat problem škálovatelnosti evaluace v oblasti evolučního návrhu a optimalizace číslicových systémů. Cílem je pomocí několika případových studií ukázat, že s využitím vhodných akceleračních technik jsou evoluční techniky schopny automaticky navrhovat inovativní/kompetitivní řešení praktických problémů. Aby bylo možné redukovat problém škálovatelnosti v oblasti evolučního návrhu číslicových filtrů, byl navržen doménově specifický akcelerátor na bázi FPGA. Tato problematika reprezentuje případ, kdy je nutné ohodnotit velké množství trénovacích dat a současně provést mnoho generací. Pomocí navrženého akcelerátoru se podařilo objevit efektivní implementace různých nelineárních obrazových filtrů. S využitím evolučně navržených filtrů byl vytvořen robustní nelineární filtr implusního šumu, který je chráněn užitným vzorem. Navržený filtr vykazuje v porovnání s konvenčními řešeními vysokou kvalitu filtrace a nízkou implementační cenu. Spojením evolučního návrhu a technik známých z oblasti formální verifikace se podařilo vytvořit systém umožňující výrazně redukovat problém škálovatelnosti evoluční syntézy kombinačních obvodů na úrovni hradel. Navržená metoda dovoluje produkovat komplexní a přesto kvalitní řešení, která jsou schopna konkurovat komerčním nástrojům pro logickou syntézu. Navržený algoritmus byl experimentálně ověřen na sadě několika benchmarkových obvodů včetně tzv. obtížně syntetizovatelných obvodů, kde dosahoval v průměru o 25% lepších výsledků než dostupné akademické i komerční nástroje. Poslední doménou, kterou se práce zabývá, je akcelerace evolučního návrhu lineárních systémů. Na příkladu evolučního návrhu násobiček s vícenásobnými konstantními koeficienty bylo ukázáno, že čas potřebný k evaluaci kandidátního řešení lze výrazně redukovat (defacto na ohodocení jediného testovacího vektoru), je-li brán v potaz charakter řešeného problému (v tomto případě linearita).
|
|
Point to Line Mappings and Other Line Parameterizations not only for Hough Transform
Havel, Jiří ; Kälviäinen, Heikki (referee) ; Lefevre, Sebastien (referee) ; Herout, Adam (advisor)
Tato práce se zabývá Houghovou transformací (HT). HT je nejčastěji používána pro detekci přímek nebo křivek, ale byla zobecněna i pro detekci libovolných tvarů. Hlavní téma této práce jsou parametrizace přímek, speciálně PTLM - zobrazení bodů na přímky. Tyto parametrizace mají tu vlastnost, že bodům v obrázku odpovídají přímky v parametrickém prostoru. Tato práce poskytuje důkazy některých vlastností PTLM. Za zmínku stojí existence páru PTLM vhodného pro detekci a efekt konvoluce v obrázku na obsah parametrického prostoru. V práci jsou prezentovány dvě implementace HT. Obě využívají k akceleraci grafický hardware. Jedna využívá GPGPU API CUDA a druhá zobrazovací API OpenGL. Jako aplikace detekce přímek je uvedena část detekce šachovnicových markerů použitelných pro rozšířenou realitu.
|
|
Multimedia Data Processing in Heterogeneous Distributed Environment
Kajan, Rudolf ; Ferko,, Andrej (referee) ; Míkovec, Zdeněk (referee) ; Herout, Adam (advisor)
Pervasive computing sa zameriava odstránenie zložitostí pri interakcii s výpočtovou technikou a zvýšenie efektivity pri jej každodennom používaní. Ale i po viac ako 15 rokoch od sformulovania hlavných cieľov Pervasive computingu existujú aspekty interakcie ktoré stále nie sú súčasťou užívateľskej skúsenosti s dnešnou technológiou. Bezproblémová integrácia s prostredím vedúca k technologickej neviditeľnosti, alebo interakcia naprieč rôznymi zariadeniami predstavujú stále veľkú výzvu. Hlavným cieľom tejto práce je prispieť k tomu, aby sa ciele Pervasive computingu priblížili k realizovaniu tým, že predstavíme spôsob intuitívneho zdieľania informácií medzi osobným a verejne umiestneným zariadením. Predstavili sme tri interakčné techniky, ktoré podporujú intuitívnu výmenu obsahu medzi osobným zariadením a zdieľaným displejom. Tieto techniky sú založené na prenose videa, rozšírenej realite a analýze pohľadových dát. Okrem interakčných techník sme tiež predstavili mechanizmus pre získavanie, prenos a rekonštrukciu aplikačného stavu na cieľovom zariadení.
|
|
Methodology of highly reliable systems design
Straka, Martin ; Gramatová, Elena (referee) ; Racek, Stanislav (referee) ; Kotásek, Zdeněk (advisor)
In the thesis, a methodology alternative to existing methods of digital systems design with increased dependability implemented into FPGA is presented, new features which can be used in the implementation and testing of these systems are demonstrated. The research is based on the use of FPGA partial dynamic reconfiguration for the design of fault tolerant systems. In these applications, the partial dynamic reconfiguration can be used as a mechanism to correct the fault and recover the system after the fault occurrence. First, the general principles of diagnostics, testing and digital systems dependability are presented including a brief description of FPGA components and their architectures. Next, a survey of currently used methods and techniques used for the design and implementation of fault tolerant systems into FPGA is described, especially the methods used for fault detection and localization, their correction, together with the principles of evaluating fault tolerant systems design quality. The most important part of the thesis is seen in the description of the design methodology, implementation and testing of fault tolerant systems implemented into FPGAs which uses SRAMs as the configuration memory. First, the methodology of developing and automated checker components design for digital systems and communication protocols is presented. Then, a reference architecture of a dependable system implemented into FPGA is demonstrated including several fault tolerant architectures based on the use of partial dynamic reconfiguration as the mechanism of fault correction and the recovery from it. The principles of controlling the reconfiguration process are described together with the description of the test platform which allows to test and verify the design of fault tolerant systems based on the methodology presented in the thesis. The experimental results and the contribution of the thesis are discussed in the conclusions.
|
|
Methodology of highly reliable systems design
Straka, Martin ; Kotásek, Zdeněk (advisor)
In the thesis, a methodology alternative to existing methods of digital systems design with increased dependability implemented into FPGA is presented, new features which can be used in the implementation and testing of these systems are demonstrated. The research is based on the use of FPGA partial dynamic reconfiguration for the design of fault tolerant systems. In these applications, the partial dynamic reconfiguration can be used as a mechanism to correct the fault and recover the system after the fault occurrence. First, the general principles of diagnostics, testing and digital systems dependability are presented including a brief description of FPGA components and their architectures. Next, a survey of currently used methods and techniques used for the design and implementation of fault tolerant systems into FPGA is described, especially the methods used for fault detection and localization, their correction, together with the principles of evaluating fault tolerant systems design quality. The most important part of the thesis is seen in the description of the design methodology, implementation and testing of fault tolerant systems implemented into FPGAs which uses SRAMs as the configuration memory. First, the methodology of developing and automated checker components design for digital systems and communication protocols is presented. Then, a reference architecture of a dependable system implemented into FPGA is demonstrated including several fault tolerant architectures based on the use of partial dynamic reconfiguration as the mechanism of fault correction and the recovery from it. The principles of controlling the reconfiguration process are described together with the description of the test platform which allows to test and verify the design of fault tolerant systems based on the methodology presented in the thesis. The experimental results and the contribution of the thesis are discussed in the conclusions.
|
|
Právní a zdravotně sociální aspekty činnosti OSPOD jako ustanovených opatrovníků v zámu nezletilých dětí
BORSKÁ, Jana
The Czech Republic as a signatory of the Convention on the Rights of the Child has vested the practice of state administration in the field of care for minor children to municipalities with extended powers, where the protection of the rights and legitimate interests of minor children is safeguarded by state authorities of social and legal protection of children (ASLPC hereinafter). These authorities are incorporated to the extent laid down by the Act on Social and Legal Protection of Children (Act No 359/1999 Coll., as amended). The position and roles of ASLPC and their competence and jurisdiction are also regulated by the same act. The position of workers of these authorities and its legal embodiment is equally important. Regarding professionality, there are high demands on these workers. In the Czech Republic, significant changes in legislature have been made over the past three years. These amendments have led to the strengthening of the rights of minor children and to the establishing of new tools for their protection. In connection with the adoption of new substantive regulation of family law, which is now exhaustively dealt with by the Act No 89/2012 Coll., the Civil Code, new procedural rules have been established regarding protection of rights of minor children. Such procedural legislation includes (apart from the long-existent Act No. 99/1963, the Code of Civil Procedure) the Act No 292/2013 Coll., on Special Civil Proceedings. The decision-making regarding minor children has been vested mainly by the state into the competence of courts. The courts appoint the locally relevant ASLPC as a guardian who then represents the interests of minor children. The purpose, interwoven with and derived from the first one, was to explore the opinions of selected social workers of ASLPC and of district court judges regarding the defined problems occurring during the work of ASLPCs and courts while protecting the interests of minor children. These particularly include: the use of the tool of precautionary measure; problems of different territorial jurisdiction of courts and ASLPCs; processing of complaints regarding bias in various phases of the proceedings; professional training of workers of ASLPC It is evident from the proposals of both judges and ASLPC workers that it is necessary to unify territorial jurisdiction. The courts are suggesting the priority criterion of the address where the child mainly resides. ASLPC workers suggest the official permanent residence as the prime criterion. Bias causes problems in all phases of proceedings. It is obvious that courts take differing approaches towards the solution of this problem (some courts solve the problem of bias complaints filed by the parties while other courts do not) and for ASLPC workers it is difficult to assess how to act when such complaint is raised against them. The training of ASLPC workers - workers are obliged to educate themselves and their employer is obliged to finance such training. Not all ASLPCs are able to provide training in the required extent - due to financial reasons (the average costs of education of one employee pose from 9,169 to 13,400 CZK annually and they cover approximately 6 days of training). The heavy work-load caused by insufficient numbers of ASLPC employees prevents them from completing such compulsory training. As part of the examination of the "participation of a collision guardian in court proceedings" it has been found out that irregular participation of the worker in the proceedings (absence from participation in appeals proceedings); incomplete reports (directed to courts) from surveys in families. Based on comprehensive examination of the problems of territorial jurisdiction, it was recommended that requests are independently recorded and financial compensation is provided for ASLPCs who are requested to represent minors in front of courts, to draft proposals for precautionary measures.
|
|
Measuring phonological awareness – blend phoneme test in the beginning of schooling: an comparison of classical test theory and item response theory
Gorčíková, M. ; Šafr, Jiří
The main purpose of this paper is to show dis/advantages of two approaches classical test theory (CTT) and item response theory (IRT) to assess the level of diagnostic tools for evaluating phonemic awareness among first-grade students using longitudinal survey of children during the first grade of primary school (25 schools in Prague and Central Bohemia, 439 pupils). Phonemic awareness (FA) was measured by the task blend phonemes into syllables and words. The advantage of IRT compared to CTT is primarily a concept of independence of the test items. The probability of a response is dependent on the level of latent ability and characteristics of items. So if we know the characteristic of items parameter (difficulty) it could be estimated from the pupil´s responses the level of language skill for diagnostics. The results showed the need for blend phoneme test modifications (in particular for the end of the first grade) so as to adequately measure the high growth of FA ability levels during the first grade.
|
|
Marketing at the shopping centre
POLÁKOVÁ, Lucie
The presented diploma thesis deals with the newly opened shopping center Galerie Teplice. The center is currently working on creation of a suitable market position with respect to the existing strong competition. The objective of the thesis is to evaluate the current position of the aforementioned shopping center on the market, then to learn more about its visitors and finally to improve targeting and personalize the marketing communication based on the analysis of results. For this reason the diploma thesis is focused on identifying and analyzing detailed information about the behavior, perceptions and preferences of visitors of designated shopping centers, especially of the Galerie center and on defining of its current positioning in relation to specified competitors.
|
|
A historical view of the army nurse profession.
PAVLÍKOVÁ, Andrea
The thesis deals with the profession of a military nurse. We can assert that the official study of military, non-medical health-care related qualifications and its use in practice not only for military purposes dates back to the fifties of the last century. However, women as health care professionals, consequently in uniforms, have always been an actual issue. The development of health care activities always existed, however, we must not neglect influence of scientific and medical findings. The historical timeline of development of medical care in the battle field was recorded and ranges from pre-historical healing. The way of Christian medicine was negatively influenced by the Catholic Church. The dark period of the Middle Ages had actually wrested medical performance from the hands of specialists and the suffering were left to the "tender" mercies of the priests. The following part of the thesis concerns modern medicine where enlightenment reforms were exercised. Some of the original six-month courses for military surgeons were organised in this period of time; they weretransformed into Military Surgical Academy, out of which the famous Josefinum originated. A expression of humanity which supported a form of health care of war veterans was demonstrated by constructing buildings for invalid people. The second half of the nineteenth century is characterized by the phenomenon of the presence of nuns in military hospitals. This study goes further in depth of professionally organized healthcare right in the battle field, which dates back from the era of wars in the Crimea.This stage describes the transformation of caring into nursing which requires the necessity of specialized preparation of persons providing nursing practice. In addition, Henry Dunant engraved himself into the history of the profession of a nurse, as the founder of the Red Cross, who first trained health care professionals for working within armed intentions of the state. The continuation of this action sketches out the process of providing first aid in principal armed conflicts of the twentieth century. It describes the functioning of commander operated military health service of that time. WWI drove Czech medical staff to both sides of the front where they provided medical help to the injured. Nurses of the WWII already performed their duties in uniforms as the rightful members of the army. The thesis also mentions post-war usage of military health care professionals in secret foreign missions and their specialized erudition.Last but not least, it marginally discusses contemporary possibilities of modern health care service of the Army of the Czech Republic. The goal of the endeavours of writing this thesis was to chart out clearly the development of the profession of a military nurse within the historical context, focusing mainly on women coming from Czech regions. In order to make the history background concerning specific female participants of the world war conflicts understandable to the reader, this paper reports, in broader extension, peculiar medical and nursing findings, already from the era of prehistoric civilisations. The history study method were applied for the purpose of the theoretical thesis. The methodology is based on searching, studying, sorting and the consecutive systematic objective describing of the events from the past times with the intention to propose comprehensive report on the subject given. It was necessary to study inexhaustible amount of sources to obtain awareness of historical connections. Factual information was derived by analysing of primary and mainly secondary documents. The thesis sketches out histories of military health care and the profession of a military health care professional stemmed from the exploration of appropriate written sources and conclusion of the basic findings. The intentions of the work are not only to clarify the past but also to contribute to solutions of every-day issues.
|
guest ::
