|
|
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)
|
|
|
Domain-Specific Language for Learning Programming
Klimeš, Jonáš ; Parízek, Pavel (advisor) ; Vinárek, Jiří (referee)
In the scope of this thesis, we designed a language for programming education. At first, we described eight existing tools for learning programming and identified key features in the learning process. Second, we designed an educational domain-specific language Eddie. Eddie is suitable for teenagers and adults who want to learn programming. It uses a domain based on Karel the Robot language, where users can control a robot character in a two-dimensional grid. We implemented a prototype of Eddie using the MPS Language Workbench and its projectional editor. The Eddie language gradually introduces loops, conditionals, variables, functions, and objects. Eddie programs can be created, executed and visualized in the Eddie Studio IDE. Powered by TCPDF (www.tcpdf.org)
|
|
|
Static analysis of C# programs
Malý, Petr ; Bednárek, David (advisor) ; Parízek, Pavel (referee)
The goal of this diploma thesis is to study and implement selected methods of static code analysis for C# programs translated into the Common Intermediate Language. The results of this work are integrated into the ParallaX Development Environment system. This diploma thesis focuses on Structural, Points-to and Dependence. analysis. Powered by TCPDF (www.tcpdf.org)
|
|
|
Bobox Runtime Optimization
Krížik, Lukáš ; Zavoral, Filip (advisor) ; Parízek, Pavel (referee)
The goal of this thesis is to create a tool for an optimization of code for the task-based parallel framework called Bobox. The optimizer tool reduces a number of short and long running tasks based on a static code analysis. Some cases of short-running tasks cause an unnecessary scheduling overhead. The Bobox scheduler can schedule a task even though the task does not have all input data. Unless, the scheduler has enough information not to schedule such task. In order to remove such short-running task, the tool analyses its input usage and informs the scheduler. Long-running tasks inhibit a parallel execution in some cases. A bigger task granularity can significantly improve execution times in a parallel environment. In order to remove a long-running task, the tool has to be able to evaluate a runtime code complexity and yield a task execution in the appropriate place. Powered by TCPDF (www.tcpdf.org)
|
|
|
Context Aware Android Application Trace Analysis
Kacz, Kristián ; Pop, Tomáš (advisor) ; Parízek, Pavel (referee)
The thesis examines how current mobile operating systems support context-aware applications and investigates the methods of mobile application debugging. The thesis points out what kind of problems need to be solved during debugging of context-aware applications. The primary goal of the thesis is to propose a debugging method which takes context information into account and to implement this method. The thesis contains a real world use case to demonstrate the proposed method.
|
|
|
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.
|
|
|
Source Code Similarity Detection
Lano, Radek ; Parízek, Pavel (referee) ; Tůma, Petr (advisor)
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.
|
|
|
Regression Benchmarking Web
Babka, David ; Parízek, Pavel (referee) ; Tůma, Petr (advisor)
During the software development the performance of the software is often important part of client requirements. Considering the constant development process of the software, comparison of the performance testing results could pinpoint to various defects in the source code, which could lead to optimizing software and its performance. This thesis focuses on implementation of flexible web application created for retrieving the performance results and presenting them in plots and other forms. The plots are dynamically generated to provide as much transparency as possible. This application will also provide the ability to send e-mails to users with the information about new measurement results.
|
|
|
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...
|
|
|
Interoperability between component-based and service-oriented systems
Mašek, Karel ; Hnětynka, Petr (advisor) ; Parízek, Pavel (referee)
The component-based and service-oriented development have become commonly used techniques for building high quality, evolvable, large systems in a timely and affordable manner. In this setting, interoperability is one the essential issues, since it enables the composition of heterogeneous components and services. The aim of the thesis is to analyze possibilities of interoperability between the SOFA2 component system and the OSGi Service Platform, and based on that propose and implement a solution for mutual collaboration. The actual integration is based on the use of aspects and annotations. The issues connected with the runtime service management (e.g. binding/unbinding services) are handled by the control part of components using the aspects. While, the annotations serve for specifying service-enabled SOFA2 components in a declarative way. The OSGi support is incorporated in both the SOFA2 runtime environment and the tool for developing SOFA2 components. Furthermore, the outlined approach is general and can be easily reused for integrating other SOA-based systems as well.
|
guest ::
