|
|
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.
|
|
|
SCXML state machine interpretter
Baláž, Ján ; Parízek, Pavel (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 specification. Work will be created in Perl and will support the operating systems Windows and Linux.
|
|
|
Model Checking and Reduction of Behavior Protocols
Šerý, Ondřej ; Bednárek, David (referee) ; Plášil, František (advisor)
Behavior protocol is a formalism used for behavior specification of software components. In a regular-expression like syntax, admissible sequences of method invocations are specified abstracting from components' internal data. While it seems to be a reasonable level of abstraction for checking correctness of communication of the software components, it can be still quite difficult for a human to read and understand. This thesis aims to help the software designer to understand the behavior specification of components more easily. An approach to automatic verification of the general temporal properties stated in Linear Temporal Logic is presented along with two techniques for reduction of behavior protocols. Reduction with respect to composition prunes out those parts of the protocols that are not used in the particular composition and vlarifies the actual role of each component. Reduction with respect to property removes the parts of the protocols that are irrelevant to the given property. The behavior protocols reduced in this manner should emphasize which part of the protocol makes the given property satisfied.
|
guest ::
RSS feed.