|
|
Movement in project ENTs
Bajer, Lukáš ; Šerý, Ondřej (referee) ; Brom, Cyril (advisor)
The ENTS project is a simulator of an environment which is similar to our common world. In this environment, there live autonomous agents called ents. They take care of their world. To fulfil their goals and satisfy their daily needs, they often have to look for a path around the world. This work is focused on scripts which are responsible for this pathfinding. The ents' movements are improved by hierarchical version of the A* algorithm. Thanks to this, demands on CPU during looking for longer paths are considerably decreased. In addition, ents' scripts are enhanced by better movement around a room, other ents following and avoiding, and "lazy" picking up objects.
|
|
|
Analyzer of Windows Kernel Models
Calta, Jan ; Šerý, Ondřej (referee) ; Ježek, Pavel (advisor)
The thesis introduces a tool for analyzing models written in the specification language DeSpec and translating them into the Zing modeling language. Resulting models can be verified by the Zing model checker. The DeSpec language is designed primarily to specify the Windows NT kernel driver environment. It makes it possible to abstract this environment in the object-oriented way and it uses temporal logic patterns to capture rules imposed by the Windows kernel on drivers. The Zing language is designed to describe executable concurrent models of software, which can be explored by the Zing model checker. Properties to check are expressed by the assertions. So far, there has been no way to automatically extract a model from DeSpec specification and verify its properties by a model checker. The DeSpec-to-Zing compiler takes a crucial part in this task. The thesis demonstrates that it is feasible to translate DeSpec specifications into Zing models and that DeSpec is a suitable language for model checking of the Windows kernel driver environment. The introduced analyzer is capable to check correctness of DeSpec specifications and under the constrained conditions given by absence of other necessary tools it is capable to translate a subset of specifications into the Zing model.
|
|
|
Memory Representation for Model Checker of C/C++
Kouba, Jan ; Kofroň, Jan (referee) ; Šerý, Ondřej (advisor)
We describe the design and C++ implementation of the newly created memory module (MM) in this work. It will be used in the GIMPLE Model Checker, an explicit state model checker, to represent the memory of checked program. MM diers from other code model checkers in the fact, that it stores ordinary C++ objects fullling a given interface as values. This allows to store, e.g., value data together with its type, a symbolic value used in a symbolic execution or a predicate over a stored value used in predicate abstraction. MM uses delta saving, incremental hashing and incremental heap canonicalization to save the state, canonicalize the heap and compute the hash of the state eciently.
|
|
|
Unit checking for Java IDE
Kebrt, Michal ; Parízek, Pavel (referee) ; Šerý, Ondřej (advisor)
Model checking programů představuje rychle se rozvíjejích oblast výzkumu. Bohužel tato technika zatím není kromě několika speciálních případů (např. veri fikace ovladačů pomocí nástroje SLAM) příliš rozšířena ve standardním procesu vývoje software. Věříme ovšem, že by mohla nastat změna, pokud by vývojáři měli možnost používat nástroje z oblasti techniky model checking podobným způsobem jako používají nástroje pro testování. Tato práce prezentuje nátroj UnitCheck, který doplňuje standardní testování Java tříd (unit testing) o metodu model checking. Vývojáři, kteří běžně využívají unit testování, mohou tento nástroj aplikovat na standardní testovací scénáře a díky části provádějící model checking (model checker) integrované v nástroji UnitCheck tak využít možnost průchodu celým stavovým prostorem daného testu. UnitCheck v sobě integruje dva dobře známé nástroje z oblasti programování v jazyce Java. JUnit je použit jako testovací framework, zatímco Java PathFinder umožňuje provádět model checking vstupních testů. Součástí celého nástroje je plugin pro prostředí Eclipse, který přehledně zobrazuje výsledky testů způsobem známým z unit testování a pokročilým uživatelům zároveň umožňuje prohlédnout si podrobnšjší informace. UnitCheck je také integrován do nástroje Ant, což umožňuje spouštět kontrolu testů (unit...
|
|
|
SCXML state machine interpretter
Baláž, Ján ; Bulej, Lubomír (referee) ; Šerý, Ondřej (advisor)
Currently there is a need for programmers to access various tasks with alternative procedures. One such practice is using the state machine entry. As the solution shows a newly emerging standard by W3 Consorcium, called SCXML. By now, there are several di fferent implementation, but because of their robustness may not be suitable for individuals or small to medium businesses. These companies need tools that can easily adapt to their own projects. The aim of this work is to create a state machine interpreter described SCXML language that will satisfy the conditions described. The e ort is to implement the maximal part of SCXML speci cation. Work will be created in Perl and will support the operating systems Windows and Linux.
|
|
|
Graphical 3D Editor for the AGE Project
Herceg, Tomáš ; Šerý, Ondřej (referee) ; Ježek, Pavel (advisor)
Title: Graphical 3D Editor for the AGE Project Author: Tomáš Herceg Department: Department of Distributed and Dependable Systems Supervisor: Mgr. Pavel Ježek, Department of Distributed and Dependable Systems Supervisor's e-mail address: pavel.jezek@dsrg.mff.cuni.cz Abstract: The goal of the thesis is to create an editor of graphical three-dimensional scenes. The editor is going to be an AGE project add-in. Because the AGE project is by the time of writing this thesis still in development its first version should be implemented as well as a part of this thesis. The 3D editor add-in should support creation of simple 3D primitives, manipulation with vertices, faces and mesh parts and also should contain basic tools for texture mapping. The Microsoft .NET Framework will be used as a target platform and all graphics content will be rendered using the Windows Presentation Foundation and DirectX technologies. Keywords: Computer graphics, Windows Presentation Foundation, DirectX, 3D
|
|
|
Economic turn-based strategy game
Hermann, Lukáš ; Šerý, Ondřej (referee) ; Lánský, Jan (advisor)
In the thesis we occupy ourselves with the design and the implementation of an economic turn-based strategy game. After describing and analyzing basic game rules we create an object model, consisting of a common interface, specifi c classes and their mutual connections. Then we analyze economic models and other related algorithms used in their methods including their transcription to a pseudo-code. Finally we create editors of properties and own behaviour of game objects and we work at creating an original graphic interface with speci c visual components which a user interface is made of.
|
|
|
Sewing pattern editor
Černý, Martin ; Poch, Tomáš (referee) ; Šerý, Ondřej (advisor)
Sewing pattern construction is a fundamental part of garment design. The subject of this thesis is the implementation of an editor of sewing patterns, that would suite the needs of independent apparel designers and custom apparel manufacturers. The editor follows closely the procedure of manual pattern design and thus is easy to use for the designer. The final program covers the most vital steps in pattern design. Patterns created in the program can be reused for different customers, since they automatically adjust to given body measures.
|
|
|
Frontend pro matematicky vyhledavac
Klíma, Jaroslav ; Mišutka, Jozef (advisor) ; Šerý, Ondřej (referee)
Mathematical notation is becoming more important as software is more often used in day-to-day life. Schools are starting to support e-learning, science is penetrating WWW and search engines can handle more complex questions. In the present work, I summarise the state-of-art of available applications which support mathematical input and could be used for graphical user interface (UI) of a mathematical search engine - EgoMath. Since none of the evaluated UIs meet our requirements, I present the design and implementation of yet another mathematical user interface focusing on the identified issues. The main goal of the new mathematical UI is to help the user provide input which will be well understood by the underlying application. Input symbols can be selected from a large domain using a limited set of keys. This must be intuitive and the application should actively aid in this task by providing graphical hints based on the input expression in real time.
|
|
|
Algorithm visualization using user-defined scripts
Šebesta, Jiří ; Šerý, Ondřej (referee) ; Ježek, Pavel (advisor)
The goal of this thesis was to create a program (AlgoShow) for explanatory chart of algorithms' process. Algorithms are written in the form of user-defined scripts that offers various functions for graphic presentation of algorithm's process. The thesis describes the program from both user's and programmer's points of view. The text includes short introduction into algorithm visualization, comparison of the AlgoShow program with another similar tools, description of design and implementation of the program including the method of script's interpretation. The thesis also includes characterization of essential program's features and detailed description of scripting language.
|
guest ::
RSS feed.