|
Methods for the measurement of bit rates in data networks
Franc, Jan ; Martinásek, Zdeněk (referee) ; Zeman, Václav (advisor)
The target of this master's thesis were the known methods for testing the quality of transfer parameters of data networks. I have studied the RFC 2544 document to analyze these tests. From that information and by studying other existing web-based applications I was able to design a concept of my own application that will allow to measure basic quality parameters of transfers made through the Internet (the parameters: downstream, upstream, latency, variance of these and a traced route). My application doesn't require any modifications on the user's system. It's built on the server-based programming language PHP and uses the relational database engine MySQL to store measurement and user data. On the client side, it's assisted by the JavaScript scripting language. Both registered users and visitors are allowed to perform the listed measurements. Registered users are able to browse the history of their own benchmark results and also to send messages to others. There is an administrative account to oversee the operations. Another part of my thesis work is an application for Windows that performs the same measurements but does not use JavaScript.
|
|
Automata in Infinite-state Formal Verification
Lengál, Ondřej ; Jančar, Petr (referee) ; Veith, Helmut (referee) ; Esparza, Javier (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zaměřuje na konečné automaty nad konečnými slovy a konečnými stromy, a použití těchto automatů při formální verifikaci nekonečně stavových systémů. Práce se nejdříve věnuje rozšíření existujícího přístupu pro verifikaci programů které manipulují s haldou (konkrétně programů s dynamickými datovými strukturami), jenž je založen na stromových automatech. V práci je navrženo několik rozšíření tohoto přístupu, jako například jeho plná automatizace či jeho rozšíření o podporu uspořádaných dat. V práci jsou popsány nové rozhodovací procedury pro dvě logiky, které jsou často používány ve formální verifikaci: pro separační logiku a pro slabou monadickou druhořádovou logiku s následníkem. Obě tyto rozhodovací procedury jsou založeny na převodu jejich problému do automatové domény a následné manipulaci v této cílové doméně. Posledním přínosem této práce je vývoj nových algoritmů k efektivní manipulaci se stromovými automaty, s důrazem na testování inkluze jazyků těchto automatů a manipulaci s automaty s velkými abecedami, a implementace těchto algoritmů v knihovně pro obecné použití. Tyto vyvinuté algoritmy jsou použity jako klíčová technologie, která umožňuje použití výše uvedených technik v praxi.
|
|
Retargetable Analysis of Machine Code
Křoustek, Jakub ; Janoušek, Jan (referee) ; Návrat,, Pavol (referee) ; Kolář, Dušan (advisor)
Analýza softwaru je metodologie, jejímž účelem je analyzovat chování daného programu. Jednotlivé metody této analýzy je možné využít i v dalších oborech, jako je zpětné inženýrství, migrace kódu apod. V této práci se zaměříme na analýzu strojového kódu, na zjištění nedostatků existujících metod a na návrh metod nových, které umožní rychlou a přesnou rekonfigurovatelnou analýzu kódu (tj. budou nezávislé na konkrétní cílové platformě). Zkoumány budou dva typy analýz - dynamická (tj. analýza za běhu aplikace) a statická (tj. analýza aplikace bez jejího spuštění). Přínos této práce v rámci dynamické analýzy je realizován jako rekonfigurovatelný ladicí nástroj a dále jako dva typy tzv. rekonfigurovatelného translátovaného simulátoru. Přínos v rámci statické analýzy spočívá v navržení a implementování rekonfigurovatelného zpětného překladače, který slouží pro transformaci strojového kódu zpět do vysokoúrovňové reprezentace. Všechny tyto nástroje jsou založeny na nových metodách navržených autorem této práce. Na základě experimentálních výsledků a ohlasů od uživatelů je možné usuzovat, že tyto nástroje jsou plně srovnatelné s existujícími (komerčními) nástroji a nezřídka dosahují i lepších výsledků.
|
|
Harnessing Forest Automata for Verification of Heap Manipulating Programs
Šimáček, Jiří ; Abdulla, Parosh (referee) ; Křetínský, Mojmír (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zabývá verifikací nekonečně stavových systémů, konkrétně, verifikací programů využívajích složité dynamicky propojované datové struktury. V minulosti se k řešení tohoto problému objevilo mnoho různých přístupů, avšak žádný z nich doposud nebyl natolik robustní, aby fungoval ve všech případech, se kterými se lze v praxi setkat. Ve snaze poskytnout vyšší úroveň automatizace a současně umožnit verifikaci programů se složitějšími datovými strukturami v této práci navrhujeme nový přístup, který je založen zejména na použití stromových automatů, ale je také částečně inspirován některými myšlenkami, které jsou převzaty z metod založených na separační logice. Mimo to také představujeme několik vylepšení v oblasti implementace operací nad stromovými automaty, které jsou klíčové pro praktickou využitelnost navrhované verifikační metody. Konkrétně uvádíme optimalizovaný algoritmus pro výpočet simulací pro přechodový systém s návěštími, pomocí kterého lze efektivněji počítat simulace pro stromové automaty. Dále uvádíme nový algoritmus pro testování inkluze stromových automatů společně s experimenty, které ukazují, že tento algoritmus překonává jiné existující přístupy.
|
|
Analysis and Testing of Concurrent Programs
Letko, Zdeněk ; Lourenco, Joao (referee) ; Sekanina, Lukáš (referee) ; Vojnar, Tomáš (advisor)
V disertační práci je nejprve uvedena taxonomie chyb v souběžném zpracování dat a přehled technik pro jejich dynamickou detekci. Následně jsou navrženy nové metriky pro měření synchronizace a souběžného chování programů společně s metodologií jejich odvozování. Tyto techniky se zejména uplatní v testování využívajícím techniky prohledávání prostoru a v saturačním testování. Práce dále představuje novou heuristiku vkládání šumu, jejímž cílem je maximalizace proložení instrukcí pozorovaných během testování. Tato heuristika je porovnána s již existujícími heuristikami na několika testech. Výsledky ukazují, že nová heuristika překonává ty existující v určitých případech. Nakonec práce představuje inovativní aplikaci stochastických optimalizačních algoritmů v procesu testování vícevláknových aplikací. Principem metody je hledání vhodných kombinací parametrů testů a metod vkládání šumu. Tato metoda byla prototypově implementována a otestována na množině testovacích příkladů. Výsledky ukazují, že metoda má potenciál vyznamně vylepšit testování vícevláknových programů.
|
|
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.
|
|
Evolutionary Approach to Synthesis and Optimization of Ordinary and Polymorphic Circuits
Gajda, Zbyšek ; Schmidt, Jan (referee) ; Zelinka,, Ivan (referee) ; Sekanina, Lukáš (advisor)
Tato disertační práce se zabývá evolučním návrhem a optimalizací jak běžných, tak polymorfních digitálních obvodů. V práci jsou uvedena a vyhodnocena nová rozšíření kartézského genetického programování (Cartesian Genetic Programming, CGP), která umožňují zkrácení výpočetního času a získávání kompaktnějších obvodů. Další část práce se zaměřuje na nové metody syntézy polymorfních obvodů. Uvedené metody založené na polymorfních binárních rozhodovacích diagramech a polymorfním multiplexovaní rozšiřují běžné reprezentace digitálních obvodů, a to s ohledem na začlenění polymorfních hradel. Z důvodu snížení počtu hradel v obvodech syntetizovaných uvedenými metodami je provedena evoluční optimalizace založená na CGP. Implementované polymorfní obvody, které jsou optimalizovány s využitím CGP, reprezentují nejlepší známá řešení, jestliže je jako cílové kritérium brán počet hradel obvodu.
|
|
Work in social integration process of adults with intellectual disability.
SVITÁKOVÁ, Iveta
In my bachelor thesis, I dealt with the use of work activities in the process of social integration of adults with mental disabilities, the aim was to create, implement and evaluate regular work activities intended to a specific group of adults with mental disability and focused primarily on the development of social integration. The thesis is structured into six chapters. The first of them is focused on the definition of mental disability, characteristic of adulthood as an important developmental period in human life, and on adulthood of individuals with mental disabilities with a goal to find and identify the specifics that were needed to be taken into account when working with this target group of people. The following section is devoted to the social integration, its determinants and the environment in which it operates. I continued with the outputs in the third chapter, where I focused on key competencies, which them are the necessary basis for social integration, especially social and personal skills and communication skills, necessary basis. Targeted professional development can be realized through educational activities, but has to respect the specificities of the participants and voluntary participation. Both of these assumptions can be fulfilled within the leisure education using adequate pedagogical methods. For this reason, I decided to focus my attention on these areas at the end of the chapter. The fourth chapter is devoted to work and work activities, namely the definition of concepts, their characteristics and importance and role of work activities in human life, or a person with mental disability. Based on all acquired theoretical knowledge and using previous experience with the target group in the fifth chapter, I designed a specific training program based on the work and activities focused on the development of selected key competences. The educational program volunteered four participants, but I have decided to follow the development of competencies of three participants because one participant attended the program very irregularly. The program has been implemented three times a week, two and a half hours for seven months (from October 2015 to May 2016) in the premises of the training centre Mo-zai-ka. At the beginning of the realisation of the created educational program, the participants agreed that we will adhere and develop good habits necessary for good relations within the group and the results of the work. On a basis of the individual characteristics of the participants, I prepared the work, which should also contribute to the development of social and personal and interpersonal skills. I have continuously monitored and recorded them. During the implementation of the program, I put emphasis on repetition, patient negotiations with participants and creating a friendly atmosphere. After completing the training program, I evaluated the development of competencies in three selected participants. On that basis, I concluded that the biggest change was in the communicative competence. I also experienced a change in social and personal competencies, however, results varied widely among individual participants. Yet, I believe that the goal of the thesis was achieved. These results show that education in leisure time, based on work activities may lead to the development of social and personal and interpersonal skills that are for adults with mental disabilities necessary in the process of social integration. This thesis can be an interesting source of inspiration for the realisation of similar programs aimed at social integration of persons with mental disabilities.
|
|
Dance as a means of integration adults with intellectual disability
KRAUMANNOVÁ, Eva
The goal of the bachelor thesis called Dance as a means of integration adults with intellectual disability was to create, implement and evaluate a dance course focused on the development of social competences in adults with intellectual disability. The thesis deals with adults with intellectual disability and with a leisure activity focused on dancing. There is some space for the development of social competences in adults´ leisure time. In response to the current situation of leisure activities proposition for adults with intellectual disability. I found it beneficial to found a dance group of adults with intellectual disability, and at the same time a group of individuals intact in places unfamiliar to them. Based on an activity which may be implemented amusingly it is possible to develop an individual´s personality as well as his or her social competences, which become a presumption of a successful integration, universally. The bachelor thesis consists of four chapters.The first chapter defines the term ´intellectual disability´. Further on the attention is paid to the characteristics of the target group, i.e. adults suffering from a slight and medium mental retardation. Further on, the disability´s impact onto the human psyche as well as social area is described. In the second chapter the term ´dance´is defined and then the description of its usefulness within the leisure, artistic and therapeutic areas is given. In the third chapter the presumptions for a successful integration are described. In the conclusion of the theoretical part there is an interconnection made between the target group and the activity for developing social competences. The theoretical part of the bachelor thesis is continued with a practical part, the fourth chapter. It is a programme of a six-month course which I have set together based on the analysis of expert literature and my experience gained during the leadership of dance lessons and working with adults with intellectual disability. The programme will include work methods and an evaluation of partial activities. The six-month course was held in the school year of 2015/2016 and 6 intellectually disabled adults took part in it. Students of the University of South Bohemia joined the course. Partial goals were set for individual dance lessons and the activities were set so that they would develop social competences in participants non-violently and in the greatest extent possible. The course was implemented in the IN Civic Association facilities. To evaluate the activity and find out the progress within the area of the participants´ social competences, several development fields have been set. Several chosen social competences were divided into evaluation scales. The participants were evaluated at the beginning of the course and then again, six months later. The evaluation method chosen was my own observation. I focused on the evaluation of my own working, on group evaluation and the evaluation of each individual. Evaluation was also done on the part of each course participant, too. Dance lessons and activities connected have proven to be a suitable means for developing social competences in intellectually disabled adults. In five participants the values have risen in 5 10 out of 17 competences observed. A recourse occured in a participant who was going through a difficult life situation during the last two months of the course. Values have risen dramatically and in all participants in the area of group cooperation. Five participants made a progress in establishing and keeping eye contact and in starting a conversation. One participant has made a progress in the area of group performance, another one has made a progress in the area of independence and another one started to call the other participants by their names, as opposed to the beginning of the course. In general, the members of the group became more self-confident.
|
|
The reflection of František Bakule's work in a relation to a current special educational practice
BALÍKOVÁ, Tereza
František Bakule was a significant Czech teacher during the first half of the 20th century. He was known as the first director of the "Jedlicka Institute in Prague" as well as the founder of so-called "Bakule´s Institute" as well as one of the few representatives of the "Czech alternative approach towards education" which is very well recognized all around the world. His legacy and teachings, however, are currently not being developed on the systematic level and neither they are being put into practise by Czech professional mainstream educational community. We also need to mention that is not used by even the stream of special education, in contrast to many foreign alternative pedagogical trends, which are gaining popularity and are generally applied with success. The aim of this thesis is therefore to analyse the work of Frantisek Bakule through the prism of contemporary school educational environment with emphasis on the education of students with disabilities. The first chapter is devoted to outlining the life journey of Frantisek Bakule, particularly focusing on the major milestones that influenced the formation of his personality, his ideas, inspiration and motivation which was reflected in his teachings and then in his very own coherent concept of education. To be specific, we are introduced to his family background and a significant part is then devoted to description of Frantisek´s experience as a teacher, including stages of operating in Jedlicka´s Institute and in his own "Bakule´s institute". The second part is then focused solely on Bakule´s specific educational concept. First, the core principles of the concept are defined. Later parts then talk about Bakule´s original curriculum and a his proposal of an ideal classroom environment. The text also contains a detailed description of how Bakule approached several subjects, which were at the core of his teaching concept, namely "Work activities", "Music education" and "Arts". Original teaching practices are analysed by using current teaching methodology and terminology. Due to the identified aim and goals of the thesis, the third chapter analyses the current concept of education of the above, according to Bakule´s core areas and principles. The text is designed specifically to be subsequently reflecting the work of Frantisek Bakule from the perspective of today's teaching methods, namely the methods of special education. The idea is to define common points and possible differences and uncover hidden inspirational potential, which is then the main content of the fourth and final chapter. Based on the analysis and all its subsequent reflections, the final chapter tells us that although Bakule´s educational goals don´t differ too significantly from the current concept embedded in the relevant framework of educational programs, to achieve such goals we are currently using very different techniques and methods in comparison to Bakule´s ways. Even though Bakule himself tested and verified all of his concepts in practice, which can be very simply described as "do not teach students about life and work, but through life and work", and these concepts also have been proven correct by various subsequent results of psychological researches, the current system still doesn´t draw from them too much. From all the above it is quite obvious that the legacy of life´s work of Frantisek Bakule is currently not utilized nor it is being appreciated by our professional pedagogical community. On the other hand, we need to note that it may also be due to the level of fragmentation in which his concept and materials were preserved to the present days.
|
guest ::
