|
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.
|
|
Trust and Reputation in Distributed Systems
Samek, Jan ; Návrat,, Pavol (referee) ; Šafařík,, Jiří (referee) ; Hanáček, Petr (advisor)
This Ph.D. thesis deals with trust modelling for distributed systems especially to multi-context trust modelling for multi-agent distributed systems. There exists many trust and reputation models but most of them do not dealt with the multi-context property of trust or reputation. Therefore, the main focus of this thesis is on analysis of multi-context trust based models and provides main assumptions for new fully multi-contextual trust model on the bases of them. The main part of this thesis is in providing new formal multi-context trust model which are able to build, update and maintain trust value for different aspects (contexts) of the single entity in the multi-agent system. In our proposal, trust value can be built on the bases of direct interactions or on the bases on recommendations and reputation. Moreover we assume that some context of one agent is not fully independent and on the bases of trust about one of them we are able to infer trust to another's. Main contribution of this new model is increasing the efficiency in agent decision making in terms of optimal partner selection for interactions. Proposed model was verified by implementing prototype of multi-agent system when trust was used for agents' decision making and acting.
|
|
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.
|
|
Vektorová segmentace objemových medicínských dat založená na Delaunay triangulaci
Španěl, Michal ; Martišek, Dalibor (referee) ; Sochor, Jiří (referee) ; Kršek, Přemysl (advisor)
Image segmentation plays an important role in medical image analysis. Many segmentation algorithms exist. Most of them produce data which are more or less not suitable for further surface extraction and anatomical modeling of human tissues. In this thesis, a novel segmentation technique based on the 3D Delaunay triangulation is proposed. A modified variational tetrahedral meshing approach is used to adapt a tetrahedral mesh to the underlying CT volumetric data, so that image edges are well approximated in the mesh. In order to classify tetrahedra into regions/tissues whose characteristics are similar, three different clustering schemes are presented. Finally, several methods for improving quality of the mesh and its adaptation to the image structure are also discussed.
|
|
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.
|
|
The Changes of agricultural Landscape of Microregion Sedlčany in the years 1850-1943
Mašková Janotová, Šárka ; Jakubec, Ivan (advisor) ; Štemberk, Jan (referee)
The thesis is focused on the economic situation development in the Sedlčany region from the first half of the 19th century till second half of the 20th century. The period observes changes from the agrarian landscape. At the end of period of the Second Czechoslovak Republic the landscape could be described as agrarian-industrial landscape. Traditionally, the Sedlčany region is considered industrially influenced. The presented thesis deals with confirmation or disproof of this idea. The research tries to find the potential focuses of dynamic economic development. If the focuses existed in the past, the research deals with comparison economic development of the Sedlčany region with other parts of Bohemia and finds the circumstances of the development. The economic situation of this area is located into wider context of the industrialization in the Czech countries during given period. Of course, the phenomenon of industrialization process relates to many factors, such as demographic development, transportation, trade, banking, agriculture and administrative activities. The federation actions are followed up in the region. The main aim of the associations is economic development of this region. They emphasize mainly upward movement of the peasant status. Keywords Sedlčany, economic history,...
|
guest ::
