|
|
Graphical 3D Editor for the AGE Project
Herceg, Tomáš ; Ježek, Pavel (advisor) ; Šerý, Ondřej (referee)
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
|
|
|
Drama manager by means of Petri Nets
Abonyi, Adam ; Brom, Cyril (advisor) ; Šerý, Ondřej (referee)
The results of virtual storytelling are used in interactive computer games or e-learning applications. The plot of a virtual story can be viewed as a distributed system, which was formalized by Carl Adam Petri in his work called Petri nets. This formalism was already used in the virtual storytelling area, but it was never used for describing a story in a virtual environment. In our work, we extend the basic Petri net model in a way which makes it easily usable for the specification of a plot of the story and for its progression. We also implement the model together with debugging tools. Moreover, we allow representing of stories using XML based format, which enables easy collaboration between the programmer and the author of the story.
|
|
|
Automated verification of software
Šerý, Ondřej ; Plášil, František (advisor) ; Janeček, Jan (referee) ; Ghezzi, Carlo (referee)
Despite the research e ort being invested into the eld of automated veri cation of software, its adoption in industry is still rather slow. Several reasons for this hesitation may be identi ed. The thesis focuses on the following two (i) dificulty of assessment of di erent tools, and (ii) difficulty of tools usage and integration in the development process. To facilitate tool assessment, we provide a comprehensive overview of code model checking techniques with evaluation based on a common set of criteria. In addition, we contribute by an industrial case study on applicability of the BLAST model checker. Since also proper education is necessary for the ability of tool assessment, we include our experience report on preparation of two master-level formal method courses. By incorporating an easy to use speci cation language into the BLAST model checker, the thesis contributes to facilitating tools usage. In addition, we introduce the concept of unit checking, a combination of unit testing and code model checking, which helps integration of code model checking in the software development process.
|
|
| |
|
|
Unit checking for Java IDE
Kebrt, Michal ; Šerý, Ondřej (advisor) ; Parízek, Pavel (referee)
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...
|
|
|
Memory Representation for Model Checker of C/C++
Kouba, Jan ; Šerý, Ondřej (advisor) ; Kofroň, Jan (referee)
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.
|
|
|
State Space Symmetry Reduction for TBP Analysis
Černý, Ondřej ; Šerý, Ondřej (advisor) ; Poch, Tomáš (referee)
Threaded Behavioral Protocols (TBP) is a specification language for modelling the behavior of software components. This thesis aims at an analysis of TBP specifications within environments which involve an unbounded replication of threads. Such a TBP specification - together with a model of the possible environments - induces infinite state space which contains a vast amount of symmetries caused by thread replication. A model checking technique addressing such a state space and reducing the symmetries by using symbolic counter abstraction is proposed. In order to utilize the symbolic counter abstraction, the properties of the TBP specifications (called provisions) are converted into thread state reachability properties. The proposed analysis is safe in the sense that it discovers all errors in the model. On the other hand, it may yield spurious errors, i.e., errors that do not correspond to any real error in the model. The spurious errors are well identified and further possibilities to reduce them are outlined. Beyond the scope of the specific specifications, this work may also present a small step towards supporting dynamic thread creation in TBP.
|
|
|
Simulátor obchodních strategií
Helešic, Tomáš ; Šerý, Ondřej (advisor) ; Poch, Tomáš (referee)
The subject of this thesis is to create a simulator for investment strategies. The resulting program allows users to download current and historical stock data, visualize it using charts and implement on it tools of the technical analysis. These components are designed and linked to create fully worthwhile environment for writing, evaluation and representation of users strategies.
|
|
|
Movement in project ENTs
Bajer, Lukáš ; Brom, Cyril (advisor) ; Šerý, Ondřej (referee)
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 ; Ježek, Pavel (advisor) ; Šerý, Ondřej (referee)
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.
|
guest ::
RSS feed.