|
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.
|
|
Grammars with Restricted Derivation Trees
Koutný, Jiří ; Janoušek, Jan (referee) ; Vojnar, Tomáš (referee) ; Meduna, Alexandr (advisor)
V této disertační práci jsou studovány teoretické vlastnosti gramatik s omezenými derivačními stromy. Po uvedení současného stavu poznání v této oblasti je výzkum zaměřen na tři základní typy omezení derivačních stromů. Nejprve je představeno zcela nové téma, které je založeno na omezení řezů a je zkoumána vyjadřovací síla takto omezené gramatiky. Poté je zkoumáno několik nových vlastností omezení kladeného na cestu derivačních stromů. Zejména je studován vliv vymazávacích pravidel na vyjadřovací sílu gramatik s omezenou cestou a pro tyto gramatiky jsou zavedeny dvě normální formy. Následně je popsána nová souvislost mezi gramatikami s omezenou cestou a některými pseudouzly. Dále je prezentován protiargument k vyjadřovací síle tohoto modelu, která byla dosud považována za dobře známou vlastnost. Nakonec je zavedeno zobecnění modelu s omezenou cestou na ne jednu, ale několik cest. Tento model je následně studován zejména z hlediska vlastností vkládání, uzávěrových vlastností a vlastností syntaktické analýzy.
|
|
Image analysis in tribodiagnostics
Machalík, Stanislav ; Stodola,, Jiří (referee) ; Tillová,, Eva (referee) ; Zemčík, Pavel (advisor)
Image analysis of wear particles is a suitable support tool for detail analysis of engine, gear, hydraulic and industrial oils. It allows to obtain information not only of basic parameters of abrasion particles but also data that would be very difficult to obtain using classical ways of evaluation. Based on the analysis of morphological or image characteristics of particles, the progress of wearing the machine parts out can be followed and, as a result, possible breakdown of the engine can be prevented or the optimum period for changing the oil can be determined. The aim of this paper is to explore the possibilities of using the image analysis combined with the method of analytical ferrography and suggest a tool for automated particle classification. Current methods of wear particle analysis are derived from the evaluation that does not offer an exact idea of processes that take place between the friction surfaces in the engine system. The work is based upon the method of analytical ferrography which allows to evaluate the state of the machine. The benefit of use of classifiers defined in this wirk is the possibility of automated evaluation of analytical ferrography outputs; the use of them eliminates the crucial disadvantage of ferrographical analysis which is its dependence on the subjective evaluation done by the expert who performs the analysis. Classifiers are defined as a result of using the methods of machine learning. Based on an extensive database of particles that was created in the first part of the work, the classifiers were trained as a result, they make the evaluation of ferrographically separated abrasion particles from oils taken from lubricated systems possible. In the next stage, experiments were carried out and optimum classifier settings were determined based on the results of the experiments.
|
|
Optimization of network flow monitoring
Žádník, Martin ; Lhotka,, Ladislav (referee) ; Matoušek, Radomil (referee) ; Sekanina, Lukáš (advisor)
The thesis deals with optimization of network flow monitoring. Flow-based network traffic processing, that is, processing packets based on some state information associated to the flows which the packets belong to, is a key enabler for a variety of network services and applications. The number of simultaneous flows increases with the growing number of new services and applications. It has become a challenge to keep a state per each flow in a network device processing high speed traffic. A flow table, a structure with flow states, must be stored in a memory hierarchy. The memory closest to the processing is known as a flow cache. Flow cache management plays an important role in terms of its effective utilization, which affects the performance of the whole system. This thesis focuses on an automated design of cache replacement policy optimized to a deployment on particular networks. A genetic algorithm is proposed to automate this process. The genetic algorithm generates and evaluates evolved replacement policies by a simulation on obtained traffic traces. The proposed algorithm is evaluated by designing replacement policies for two variations of the cache management problem. The first variation is an evolution of the replacement policy with an overall low number of state evictions from the flow cache. The second variation represents an evolution of the replacement policy with a low number of evictions belonging to large flows only. Optimized replacement policies for both variations are found while experimenting with various encoding of the replacement policy and genetic operators. The newly evolved replacement policies achieve better results than other tested policies. The evolved replacement policy lowers the overall amount of evictions by ten percent in comparison with the best compared policy. The evolved replacement policy focusing on large flows lowers the amount of their evictions two times. Moreover, no eviction occurs for most of the large flows (over 90%). The evolved replacement policy offers better resilience against flooding the flow cache with large amount of short flows which are typical side effects of scanning or distributed denial of service activities. An extension of the replacement policy is also proposed. The extension complements the replacement policy with an additional information extracted from packet headers. The results show further decrease in the number of evictions when the extension is used.
|
|
The Pump with a Diffuser with Stochastic Blades (Runner and Diffuser)
Dobšáková, Lenka ; Melichar, Jan (referee) ; Veselý, Jindřich (referee) ; Haluza, Miloslav (advisor)
This doctoral thesis studies the non-uniform blade cascade for centrifugal pumps. Influence of non-uniform blade cascade is investigated on the impeller and diffuser. A non-uniform blading impeller of pumps in this doctoral thesis was examined in terms of influence on efficiency characteristic. The idea of using non-uniform blading is to obtain a flat efficiency characteristic. Then the centrifugal pump could be used on larger scale of power with achieving a sufficiently high efficiency. The work is based on experimental measurements and numerical simulations of non-uniform hydraulic pump components. Non-uniform impeller and the diffuser were newly designed for this research. A new measuring track of small submersible pumps was needed to design and build for measurements. Different pump combinations with conventional hydraulics on one working point and hydraulics with non-uniform were measured. All measurements were evaluated and characteristics of efficiency, head and power were obtained for each measured combination. Some of pump combinations (which were measured in experiment) were numerically simulated by program Ansys Fluent. Data needed to evaluate the characteristic of efficiency and specific energy were collected from each numerical simulation. A theoretical consideration concerns the influence of non-uniform blade cascade applied on diffuser. The suggestion how to decrease hydraulic losses in canals was done. The theoretical consideration how to make a flat efficiency characteristic was made.
|
|
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.
|
|
Are There Any Digital Curators in Czech Libraries?
Římanová, Radka ; Melichar, Marek
The development of digital repositories reveals the need for new Czech terminologies for library positions. One such job title or specialization is “digital curator”, a term which refers to a specialist responsible for digital collections. Competencies for digital curators include technical, organizational, communication, and marketing skills as well as some level of expertise in computer science as well as in information and library science. A survey of several administrators of Czech digital libraries asks how to best professionally label this group of library staff with respect to the actual activities they perform in their jobs - digital curators, administrators of digital libraries, or digital librarians? Job titles have a strong impact on higher education curricula, on the management of libraries, and also on the coordinated system of remuneration of employees at libraries, academic, and research institutions.
Fulltext: idr-1041_3 -  PDF; idr-1041_4 - PDF
Slides: idr-1041_1 - PDF; idr-1041_2 - PDF
Video: idr-1041_5 -  MP4
|
|
Ratings business accounts
ŠUSTROVÁ, Lucie
The diploma thesis is focused on using methods of multiple criteria decision making, in this case about business accounts. In theoretical part is described the banking systém of Czech republic, then methods of multiple criteria evaluation.The basic aim of this work was to evaluate the order of business accounts in terms of advantageousness, which are offered by banks on the banking market in the Czech republic. The sectional aim of this work is to get known with the problems of optimal choice of business accounts for a certain group of consumers, which in this case are small businesses. Before choosing a new business account it is always necessary to carefully explore banking market and its offers of business accounts. The important part of this thesis is that the certain client has to consider his preferences before we use quantitative methods. In this diploma thesis has also done a survey about the evaluation of business accounts. Then there are compared results of using methods of multiple criteria evaluation of the survey and model client. In conclusion, the results are described in the order of banking products from the best to the worst business account.
|
|
Methods of transfer pricing by multinational enterprises in terms of tax administration
BÖHMOVÁ, Dana
The aim of the thesis is the analysis and evaluation of the application of transfer (transfer) the prices used in transactions of multinational enterprises in terms of tax administration. Generally describe the basic principles of the United people, the principle of the arm, the methods of the determination of the transfer pricing and documentation for transfer prices in accordance with the international rules and standards laid down by the Organization for economic cooperation and development, in accordance with the laws and guidelines of the Czech Republic. Furthermore, this thesis seeks to clarify the specific case studies, which are based on the practice of financial management, and the case-law, the effects of the determination of the transfer pricing methods, comparison of their advantages and disadvantages in establishing transfer prices in the Czech Republic. At the conclusion of the thesis summed up the results and recommend the adoption of more appropriate legislation in each of the areas of transfer pricing in the Czech Republic.
|
|
Small Size Municipality Revenues in Czech Republic
JIREKOVÁ, Kateřina
The aim of this thesis is to evaluate the system of municipality incomes in the Czech Republic with respect to specifics of small municipalities. In last few years these municipalities have become a frequently discussed topic because of their lower incomes. The legislation has been devoting to this problem since 2008 and the differences between large and small municipalities in the Czech Republic were removed. There is income analysis of all municipalities in the Czech Republic from 2000 up to 2012 in this thesis. The municipalities were divided into two groups. The first group contains small villages, defined as municipalities up to 499 inhabitants. In the second group there are other municipalities of the Czech Republic except small villages, statutory cities and the Capital City of Prague. The real data were recalculated per head for this analysis and minimum, maximum, median and arithmetic mean were found. Variability of incomes is evaluated from these results. Regression and correlation analysis is made in some groups of revenues because of finding dependence among variables. Disparity in incomes of small towns and other communities is assessed by comparing the arithmetic means and medians between groups of municipalities using a Two-Sample t-test and Mann-Whitney test. Revenue growth is evaluated determination of the trends of the time series using linear regression. Some specifics in financing small villages were found from these analyzes. There was also confirmation of the hypothesis that small municipalities have lower incomes per an inhabitant.
|
guest ::
