|
|
Vector editor for creating animations
Kruliš, Martin ; Zavoral, Filip (advisor) ; Parízek, Pavel (referee)
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.
|
|
|
Checking Primitive Component Behavior
Klika, David ; Kofroň, Jan (advisor) ; Parízek, Pavel (referee)
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.
|
|
|
Universal Interconnection of Electronic Health Records and Formalized Electronic Medical Guidelines
Húska, Jakub ; Nagy, Miroslav (advisor) ; Parízek, Pavel (referee)
The purpose of this thesis is to design a universal bridge between any Electronic Health Record (EHR) and formalized medical guidelines included in evaluation and presentation system. The interconnection should ensure medical data for medical guidelines that are evaluated. These data should be acquired from EHR using standard techniques, if possible. To solve the thesis there are some systems ready to be used: the medical guidelines evaluating and presenting system named "Medical Guidelines SYSTEM"[1] and an EHR named AdamekJ based on the MUDRLite2 technology. The solution should be designed in a modular way in order to connect various EHRs and medical guidelines systems. The programming language and other supportive technologies necessary for completing the task can be chosen by a student.
|
|
|
Formal Verfication of Components in Java
Parízek, Pavel ; Plášil, František (advisor) ; Černá, Ivana (referee) ; Pasareanu, Corina (referee)
Formal veri cation of a hierarchical component application involves (i) checking of behavior compliance among sub-components of each composite component, and (ii) checking of implementation of each primitive component against its behavior speci cation and other properties like absence of concurrency errors. In this thesis, we focus on veri cation of primitive components implemented in Java against the properties of obeying a behavior speci cation de ned in behavior protocols (frame protocol) and absence of concurrency errors. We use the Java PathFinder model checker as a core veri cation tool. We propose a set of techniques that address the key issues of formal veri cation of real-life components in Java via model checking: support for high-level property of obeying a behavior speci cation, environment modeling and construction, and state explosion. The techniques include (1) an extension to Java PathFinder that allows checking of Java code against a frame protocol, (2) automated generation of component environment from a model in the form of a behavior protocol, (3) efficient construction of the model of environment's behavior, and (4) addressing state explosion in discovery of concurrency errors via reduction of the level of parallelism in a component environment on the basis of static analysis of Java...
|
|
|
Java Bytecode Preprocessor for Program Verification Tools
Šafařík, Tomáš ; Parízek, Pavel (advisor) ; Hnětynka, Petr (referee)
Both J2BP and PANDA tools verify compiled Java programs. By now, these tools are not able to process some programs with specific JVM bytecode instruction sequences in the correct way. We described these instruction sequences and proposed their transformations. We developed the new application, called BytecodeTransformer, based on these propositions. This application transforms compiled Java programs and replaces the problematic instruction sequences with some others. Usage of BytecodeTransformer enlarges the set of programs that can be verified by both J2BP and PANDA. We also evaluated BytecodeTransformer on several Java programs, including own tests and well-known open-source programs. These tests demonstrated the correct functionality of BytecodeTransformer. Powered by TCPDF (www.tcpdf.org)
|
|
|
Source Code Similarity Detection
Lano, Radek ; Tůma, Petr (advisor) ; Parízek, Pavel (referee)
The objective of this thesis is to design and implement a tool usable for detecting similar code in different projects. The tool should be able to locate code pasted from one project to another and should be able to cope with average attempts to thwart the detection such as symbol renaming, changing the order of unrelated entities, moving entities to different files, adding or removing comments, etc. The tool is implemented in language C++ and is ready to compare source files written in languages C and C++. The tool also enables the comparison of source code written in different languages, which can be compiled by the GNU C Compiler. To obtain good results in these cases, new modules should be added (this is necessitated due to different representations of the GNU C Compiler inner form for different languages). The first part of this thesis focuses on describing the problem domain, the architecture design and the tools usable for implementation. The second part centers on the implemented solution, a description of data structures and possibilities for application expansion using additional modules. The last part of the thesis sums up the results and outlines future possibilities of implementation.
|
|
| |
|
|
Using Java PathFinder for Construction of Abstractions of Java Programs
Yuldashev, Nodir ; Parízek, Pavel (advisor) ; Poch, Tomáš (referee)
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.
|
|
|
Checking Compliance of Java Implementation with TBP Specification
Jančík, Pavel ; Parízek, Pavel (advisor) ; Kofroň, Jan (referee)
Verification is a method of increasing reliability of component based applications. Component composition and its verification from the communication point of view, is one of the current research topics. Behavior protocols (BPs) are an abstraction used to describe communication among components. Tools, that are able to verify component composition, have already been developed. These tools concern only the BP level and they implicitly presume that implementation of the components conforms to given BP. The importance of verification of implementation compliance with BP is obvious. The BP and rules for communication among components are created during the early steps of the development cycle. Various deviations from the original BP (intentional or unintentional) arise during the implementation phase. This approach reflects the importance of a checker tool. Checker tool, which will ensure conformance of a single component implementation written in Java with given threaded behavior protocol, is the final result of our work. The work also contains an evaluation of the tool in bigger real life examples.
|
|
|
Automated detection of vulnerabilities in web applications
Tomori, Rudolf ; Parízek, Pavel (advisor) ; Babka, Vlastimil (referee)
Security vulnerabilities, while being an important and common problem of web applications, are often easily detectable by using specialised software. The WebCop tool developed in this thesis is able to spot some of the common web application security vulnerabilities. Its main advantage over other similar software lies in its ability to configure the way in which the individual tests are performed, also allowing the user to specify the conditions that are required to be met in order to acknoledge the presence of the given security vulnerability. The tool is developed for the Unix/Linux platform using the C++ language.
|
guest ::
RSS feed.