|
|
Presenting results of software model checker via debugging interface
Kohan, Tomáš ; Šerý, Ondřej (advisor) ; Jančík, Pavel (referee)
Title: Presenting results of software model checker via debugging interface Author: Tomáš Kohan Department: Department of Software Engineering Supervisor of the master thesis: RNDr. Ondřej Šerý, Ph.D., Department of Distributed and Dependable Systems Abstract: This thesis is devoted to design and implementation of the new debugging interface of the Java PathFinder application. As a suitable inte- face container was selected the Eclipse development environment. The created interface should visualize results of JPF and details of paused JVM state, es- pecially a list of variables and their values. Two subprojects were created, i.e. debug4jpf and JPFDeb.core. The first one is responsible for controlling and communication with the JPF instance. The latter one is an Eclipse plugin and provides user interface which is similar to the interface of standard Java debugger. These two components communicate with each other by using the ad-hoc communication protocol created for this purpose. Keywords: Java, verification, model checker, JPF, debugging interface
|
|
|
Presenting results of software model checker via debugging interface
Kohan, Tomáš ; Šerý, Ondřej (advisor) ; Jančík, Pavel (referee)
Title: Presenting results of software model checker via debugging interface Author: Tomáš Kohan Department: Department of Software Engineering Supervisor of the master thesis: RNDr. Ondřej Šerý, Ph.D., Department of Distributed and Dependable Systems Abstract: This thesis is devoted to design and implementation of the new de- bugging interface to the Java PathFinder application. As a suitable interface container was selected the Eclipse development environment. The created inter- face visualizes results of JPF and details of paused JVM state, especially a list of variables and their values. Two subprojects were created, i.e. debug4jpf and JPFDeb.core. The first one is responsible for controlling and communication with the JPF instance. The latter one is an Eclipse plugin and provides user interface which is similar to the interface of standard Java debugger. These two components communicate with each other by using the ad-hoc communication protocol created for this purpose. Keywords: Java, verification, model checker, JPF, debugging interface
|
|
|
CMS Supporting Dynamically Generated Content
Nádraský, Václav ; Ježek, Pavel (advisor) ; Šerý, Ondřej (referee)
The topic of this thesis covers design and development of content management system which is easily extensible. It allows creating websites out of components which can be placed at any place in a web site. These components can contain a complex application logic which is independent of a layout of user controls. Content management system also contains a component allowing to place any data from any database into web site content without need to program or to create SQL queries.
|
|
|
Vector Graphics Editor for the AGE Project
Šebetovský, Jan ; Ježek, Pavel (advisor) ; Šerý, Ondřej (referee)
Present work studies possibilities of creating the vector graphics editor, which would be able to work as part of project AGE. Purpose of this project is to create integrated graphics tool. This work also contains program which is basic version of described editor. The advantage of this editor is especially ability to compute dimensions and colours of objects in picture from properties of another objecet in picture according to expression created by user. Editor also supports layers (in form of groups of objects), export of picture into bitmap formats and ability to work with Bézier curves. In addition this program almost fully supports filters, which are created in other work.
|
|
|
Investment Strategies Simulator
Helešic, Tomáš ; Šerý, Ondřej (advisor) ; Poch, Tomáš (referee)
Title: Investment Strategies Simulator Author: Tomáš Helešic Department: Department of Software Engineering Supervisor: RNDr. Ondřej Šerý Supervisor's e-mail address: ondrej.sery@d3s.mff.cuni.cz Abstract: The goal of this thesis is the creation of an investment strategies simulator. The resulting program allows users to download current and historical stock data, visualize it using charts and implement on it the tools of technical analysis. These components are designed and linked to create fully worthwhile environment for the creation, evaluation and representation of user strategies. Keywords: Investment strategies; Technical analysis, Scripting;
|
|
|
Software pro rozvrhování operací a evidence nástrojů pro nemocniční zařízení
Tupec, Pavel ; Šerý, Ondřej (advisor) ; Kruliš, Martin (referee)
Nowadays in most medical facilities is daily schedule of operations mainly created manually or with minimal support of software tools. Result of this is occasional ineffectivity of operation schedule and primarily huge time consumption for surgery chief who could use his time for more important things related to his work. Another reason for creating this application is that information about patients, operations, wards and diagnosis are stored decentralized in different applications and systems, which makes working with them more difficult. Target of this application is implementation application for creating operating schedules in hospital facilities with assurance of necessary instruments, wards and instrument evidence. Where all data about all necessary entities will be stored and managed centralized. Purpose of final program is make schedule creating more effective and partially automatized operation planning.
|
|
|
Model Checking and Reduction of Behavior Protocols
Šerý, Ondřej
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 clarifies 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.
|
|
|
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.
|
|
|
GIMPLE Model Checker
Krč-Jediný, Ondrej ; Šerý, Ondřej (advisor) ; Hauzar, David (referee)
Title: GIMPLE Model Checker Author: Ondrej Krč-Jediný Department: Department of Distributed and Dependable Systems Supervisor: RNDr. Ondřej Šerý Ph.D. Supervisor's e-mail address: Ondrej.Sery@mff.cuni.cz The goal of the thesis is a prototype implementation of explicit-state model checker of C - an advanced tool for finding errors in programs. This tool ex- plores all possible paths of program execution as well as all thread interleavings. It is based on GIMPLE - output of front-end of GCC compiler, which is the input language for GMC. The thesis is based on the previous work 'Memory represen- tation for GIMPLE Model Checker', that implements work with memory for this tool. Since it is based on GIMPLE, it makes it possible to verify systems directly in C. In addition, it is easily extensible to other languages supported by GCC. Keywords: model checking, GIMPLE, GCC, C 1
|
|
|
Group Time Manager
Florián, Jiří ; Žemlička, Michal (advisor) ; Šerý, Ondřej (referee)
Whether you want to admit it or not, our whole life consists of the performance of various tasks and events. And just a draft application for easy scheduling of tasks and events is the aim of this thesis. Specifically, it will be a program that is suitable for both personal and work related planning occurred without any invasion of privacy.
|
guest ::
RSS feed.