|
|
Safe e-shop
Hejl, Tomáš ; Parízek, Pavel (referee) ; Mišutka, Jozef (advisor)
This thesis describes the common types of attacks against web applications and web pages in general, the protective measures against them and the specific application of these measures in the e-shop. The goal of this thesis is the safe application using common resources, without using third-party frameworks or existing solutions.
|
|
|
Vector editor for creating animations
Kruliš, Martin ; Parízek, Pavel (referee) ; Zavoral, Filip (advisor)
The object of this work is to design and implement a vector editor with animation support. This program is designated for a very specialized group of users that want to create simple animations but find buying complex commercial tools unnecessary. The application will allow user to design basic vector objects, edit them and set them into motion using curved trajectories. Main features of the application are its modularity and flexibility, making it ready for future extending and customization.
|
|
|
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.
|
|
|
Using Java PathFinder for Construction of Abstractions of Java Programs
Yuldashev, Nodir ; Poch, Tomáš (referee) ; Parízek, Pavel (advisor)
The growing complexity of software systems makes the verification of the systems very difficult. Techniques of formal verification and analysis are used to find bugs in the code, or to prove that the code satisfies some properties. A popular automated verification technique is model checking, which uses state space traversal. However, model checking is prone to state explosion and therefore does not scale to complex multi-threaded software systems. Common solution to this problem (state explosion) is to create an abstraction of the target system, and then verify only the abstraction. We have designed and implemented a tool for construction of abstraction of Java components in behavior protocols, which is based on the Java PathFinder model checker. Results of experiments on several non-trivial components show that the tool can be used in practice.
|
|
|
Traffic monitoring in TCP/IP networks
Bouška, Zdeněk ; Malohlava, Michal (referee) ; Parízek, Pavel (advisor)
The subject of this work is a tool for monitoring of traffic in a TCP/IP network. The tool provides information about speci c TCP connections and packets, and also displays various statistics. It is possible to apply lters on all information related to TCP connections and packets. The tool supports both graphical and text user interface, and also traffic monitoring on remote computers. The tool is implemented in C++ and runs on GNU/Linux.
|
|
|
Checking Primitive Component Behavior
Klika, David ; Parízek, Pavel (referee) ; Kofroň, Jan (advisor)
Software model checking is a process of checking for properties of a software application and thus assuring the software reliability. It is still necessary to divide the software application into pieces that are checked separately; the whole application yields an enormous state space that is impossible to traverse in a reasonable time. Therefore, the use of components is a straightforward approach for dividing the entire application. Furthermore, as model checker usually works with a close code only, a suitable component environment need to be provided for each component. Behavior protocols are a method for component behavior specification. They allow for checking for components' behavior compatibility and compliance, used at the design time of an application to find possible architectural component misplacements. They are also suitable to be compared with the behavior of the component implementation. The goal of the thesis is to provide a tool for comparing a primitive component behavior with its specification. Furthermore, a component environment generator using the component frame protocol will be implemented that would enable for checking for violation of the component behavior specification. The Java PathFinder model checker and the Fractal component model are to be used as a model checking platform.
|
|
|
Steganographics filesystem
Kollár, Ivor ; Parízek, Pavel (referee) ; Holub, Viliam (advisor)
In the present work we study protecting of information in situations, when cryptography alone is not enough. We will try to analyze possibilities of information hiding, not in innocent looking carrier of information (sound, picture, video), but in pseudosteganographic archive. We will try to describe (and later implement) algorithm, that will be able to create archive, meeting following conditions: Archive will contain N les, each protected by one key. Number N must remain hidden to attacker. By using one of keys, we will get only one le, getting no information about rest of les in archive. Implementation of this algorithm should be as simple as possible,maximally platform independent, and easily practically usable.
|
|
|
Transactions in Peer-to-Peer Systems
Parízek, Pavel
The thesis begins with discussion of usability of transactions in peer-to-peer environment, with the result that transactions are useful for some kinds of peer-to-peer applications, and specifies requirements on transaction coordination protocol that is suitable for peer-to-peer environment. After that, introductions to the JXTA peer-to-peer platform and to the BTP coordination protocol follow. The last part of the thesis is devoted to the BTP-JXTA framework, which I have developed. The framework extends the JXTA platform with a transaction service that uses the BTP as its coordination protocol. The description of the framework focuses on architecture and important implementation concepts and on the methodology of testing that was used.
|
|
|
Music typesetting program
Hanslík, Ondřej ; Parízek, Pavel (referee) ; Holan, Tomáš (advisor)
Aim of this work is to design and implement application, which would transform MIDI data into music notation suitable for printing. Correct division of the music document to pages and fulfilment of notation standards is essential. Application would offer these features: - acceptance of every MIDI file that fulfils the SMF specification - possibility to choose which parts in the MIDI file will be imported - wide possibilities of editing the loaded document - support for the majority of signs used in music - different methods of dividing the document to pages - page head and foot Application will be built on platform .NET Framework, implementation language will be C#.
|
|
|
Code Assertions Verification Using Backward Symbolic Execution
Husák, Robert ; Kofroň, Jan (advisor) ; Parízek, Pavel (referee)
In order to prevent, detect and fix errors in software, various tools for programmers are available, while some of them are able to reason about the behaviour of the program. In the case of C# programming language, the main representatives are Microsoft FxCop, Code Contracts and Pex. Those tools can, indeed, help to build a highly reliable software. However, when a company wants to include them in the software development process, there is a significant overhead involved. Therefore, we created a "light- weight" assertion verification tool called AskTheCode that can help the user to focus on a particular problem at a time that needs to be solved. Because of its goal-driven approach, we decided to implement it using backward symbolic execution. Although it can currently handle only basic C# statements and data types, the evaluation against the existing tools shows that it has the potential to eventually provide significant added value to the user once developed further. Powered by TCPDF (www.tcpdf.org)
|
guest ::
