|
|
Verification of Textual Use-Cases
Vinárek, Jiří ; Šimko, Viliam (advisor) ; Hauzar, David (referee)
The aim of this thesis is to create a tool for formal verification of systems specified using textual use- cases. The tool should allow for automated verification of temporal invariants specified in temporal logic (CTL and LTL formulae). The textual specification is transformed to a formal model that is verified using the NuSMV symbolic model-checker. Potential errors are shown to the user in the form of an HTML report. Using this feedback, the user is able to iteratively develop valid textual use-case specifications. The tool's architecture should be focused on reusability of its components and extensibility. Powered by TCPDF (www.tcpdf.org)
|
|
|
Qt HDD benchmark
Matěna, Vladimír ; Marek, Lukáš (advisor) ; Šimko, Viliam (referee)
This thesis deals with data storage device benchmarking. Its purpose is to provide storage device benchmarking application with graphical user interface for Linux environment. The graphical interface is simple to use and displays results in real-time. Moreover a few common device benchmarking was done with application developed. The interesting results were briefly described as well as factors influencing them. Also general factors impacting results measured within the Linux environment were described.
|
|
|
IDE-supported development of component-based applications
Hermann, Lukáš ; Bureš, Tomáš (advisor) ; Šimko, Viliam (referee)
Unlike many proprietary component systems, the academic ones do not have sufficient support in integrated development environments. This the- sis analyzes development of component-based applications in terms of the SOFA 2 component system and it finds out that the main issue is an in- sufficient connection between processes of common application design and creation of particular components. Based on this analysis, it defines a subset of the UML, a universal language for application design, and its semantics regarding entities of the SOFA 2 component system. Furthermore, it creates a tool integrated to the Eclipse IDE, which enables a developer to automat- ically generate these entities from a UML component model as well as to connect this model with already existing entities enabling their automatic correction in case of model changing. This tool is designed modularly so that it is possible to easily change semantics of the model or using it for other models. Finally, this thesis analyzes possibilities of extensions of this tool for other component systems, code generation and component behaviour verification.
|
|
|
Roulette Gambling
Vlk, Marek ; Malohlava, Michal (advisor) ; Šimko, Viliam (referee)
This work goes into roulette gambling. Its pivotal intension is to design and implement this game. The application provides two playing modes: "training game" working o -line and "real game" that performs multi-player game on-line. The work takes a focus on speed and reliability of network communication and on user-friendly 3D casino environment. Furthermore, the program provides playing and simulation of game systems implemented in the program and allows importing own system. The application is written in C# language for Windows platform. Network communication is realized via .NET Remoting.
|
|
|
Multimedia Grid
Šimko, Viliam
The thesis describes the possibilities and issues of existing videoconferencing systems. We focus on open-source solutions for group-to-group communication especially the AccessGrid technology that utilizes the multicast packet delivery method of multimedia content. We describe AccessGrid node created for CIANT organization, which has been taken as a starting point for defining the architecture of a videoconferencing system based exclusively on open-source components, particularly Linux and related software. We address issues related to firewalls and NAT traversal and provide a comparison of various videoconference-related codecs and protocols. Finally, the text touches the question of recording and archiving of conference sessions and provides a new integrated recording application -- StreamVNC. The tool allows users to prepare their presentations using localhost recording facility which includes AGVCR for recoding RTP packets, EVIC for grabbing the VNC display and camera source and RAT as an audio encoder.
|
|
|
Multimedia Grid
Šimko, Viliam ; Galamboš, Leo (advisor) ; Jirovský, Václav (referee)
The thesis describes the possibilities and issues of existing videoconferencing systems. We focus on open-source solutions for group-to-group communication especially the AccessGrid technology that utilizes the multicast packet delivery method of multimedia content. We describe AccessGrid node created for CIANT organization, which has been taken as a starting point for de ning the architecture of a videoconferencing system based exclusively on open-source components, particularly Linux and related software. We address issues related to rewalls and NAT traversal and provide a comparison of various videoconference-related codecs and protocols. Finally, the text touches the question of recording and archiving of conference sessions and provides a new integrated recording application { StreamVNC. The tool allows users to prepare their presentations using localhost recording facility which includes AGVCR for recoding RTP packets, EVIC for grabbing the VNC display and camera source and RAT as an audio encoder.
|
|
|
Syntax-based extraction of component behavior specifications
Reidinger, Josef ; Šimko, Viliam (referee) ; Poch, Tomáš (advisor)
There is a component based paradigm which can be used for large software systems. It has advantage that its parts - components can be resused and if contain behavior description it allows many behavior analyses. A component contains static description of interface for reusing and optionally behavior description for correctness analyses. It is possible to further analyze behavior description whether a component does not break restrictions of the required components, whether the resulted behavior is the expected one and whether all components fit together. Behavior description defines restrictions on component methods and how it reacts to an invocation of method. The reactions specify order and workflow of invoking methods from the required interfaces. Manual writing of component behavior is prone to bugs and it should be automated. The result of this work is a tool which can generate automatic behavior description from the source code that does not violate restrictions. The tool can be used to add behavior description during transformation legacy systems to component based ones or to check how source code changes affect behavior description. The work also contains an evaluation of possible technologies which can be used for analysis. The tool is a part of the international Q-Impress project and uses other...
|
guest ::
RSS feed.