|
|
Efficient Algorithms for Finite Automata
Hruška, Martin ; Rogalewicz, Adam (referee) ; Lengál, Ondřej (advisor)
Nondeterministic finite automata are used in many areas of computer science, including, but not limited to, formal verification, the design of digital circuits or for the representation of a regular language. Their advantages over deterministic finite automata is that they may represent a language in even exponentially conciser way. However, this advantage may be lost if a naive approach to some operations is taken, in particular for checking language inclusion of a pair of automata, the naive implementation of which performs an explicit determinization of one of the automata. Recently, several new techniques for this operation that avoid explicit determinization (using the so-called antichains or bisimulation up to congruence) have been proposed. The main goal of the presented work is to efficiently implement these techniques as a new extension of the VATA library. The implementation has been evaluated and is superior to other implementations in over 90% of tested cases by the factor of 2 to 100.
|
|
|
Generating Tree Structures for Testing of Information Systems
Rozsíval, Michal ; Hruška, Martin (referee) ; Smrčka, Aleš (advisor)
The work aims to create a tool for automated testing of information systems. It creates messages similar in structure to those in the communication of existing systems. The program reads provided communication record according to configuration and saves the individual messages in a uniform form. It splits the saved messages into groups and abstracts them into a suitable form for a subsequent generation of new random test messages based on a combinatorial testing with Pair-Wise coverage. The tool supports communication using the REST API and OPC UA protocols and structured data in XML and JSON . The program was tested by processing real communication records.
|
|
|
Automated Detection of Types in Data Structures
Oháňka, Martin ; Hruška, Martin (referee) ; Smrčka, Aleš (advisor)
This bachelor's thesis deals with data structure synthesis for software testing. In particular, the thesis focuses on analysis of real data in order to detect data types for further test data generation. Data analysis is performed in two layers: a control system for scheduling and invoking partial detections, and a set of data detectors. The thesis deals with analysis and implementation of tool consisting of set of data type detectors over tree structured data like JSON, YAML, or XML. The goal of the detectors is to determine a semantics of values of analysed structure and dependencies between data. The set can be easily expanded as needed, to detect even more complicated meanings and dependencies. The results of these analysis can be used to generate new test data for software testing.
|
|
|
An Efficient Functional Library for Finite Automata
Říha, Jakub ; Hruška, Martin (referee) ; Lengál, Ondřej (advisor)
Finite automata are an important mathematical abstraction, and in formal verification, they are used for a concise representation of regular languages. Operations often used on finite automata in this setting are testing their universality and language inclusion. \mbox{A naive} approach to implement these operations leads to an explicit determinization of the automata, which can be costly and undesirable. There is, however, a more advanced method for performing those operations, called the Antichains algorithm, which avoids such an explicit determinization. This work shows how finite automata operations can be effectively implemented in Haskell and compares several approaches of their implementation. The obtained results are compared with VATA, an imperative implementation of a finite automata library.
|
|
|
Efficient Algorithms for Tree Automata
Valeš, Ondřej ; Hruška, Martin (referee) ; Lengál, Ondřej (advisor)
In this work a novel algorithm for testing language equivalence and inclusion on tree automata is proposed and implemented as a module in the VATA library. First, existing approaches to equivalence and inclusion testing on both word and tree automata are examined. These existing approaches are then modified to create bisimulation up-to congruence algorithm for tree automata and a formal proof of the soundness of the new algorithm is provided. Efficiency of this new approach is compared with existing language equivalence and inclusion testing methods for tree automata, showing the performance of our algorithm on hard cases is often superior.
|
|
|
Wireless sensor network
Hruška, Martin ; Burda, Karel (referee) ; Mišurec, Jiří (advisor)
Wireless sensor network (WSN) consist of a mesh of a several powerful devices (denoted as base stations or sink) and a high number (1000 - 1000000) of a low-cost devices (denoted as nodes or motes), which are severely constrained in processing power, memory and energy. The nodes are equipped with an environment sensor. Events recorded by the sensor nodes are locally aggregated and then forwarded to a base station for further processing. WSNs are expected to be in wide use for a multitude of different scenarios. Project target is to analyse possibility of wireless transfer of digitalised data from sensors. Work contains and compares: Wi-Fi, , WiMAX, ZigBee, GPRS, radio net and IrDA. The work will design a wirelless network with data collection from sewerage plant sensors in small rural agglomeration and transfer data to the central dispatching. The work will suggest several options and compare their advantages and disadvantages.
|
|
|
Continues Integration Support for Copr Build System
Klusoň, Martin ; Hruška, Martin (referee) ; Rogalewicz, Adam (advisor)
This thesis deals with implementation of continuous integration for build system Copr. The implementation uses framework Citool and its modules, which are already used for continuous integration of build system Koji. The outcome system can run the tests for the new package from the build system Copr and test it on virtual machine. This thesis shows way how to implement continuous integration for build system Copr.
|
|
|
Tool for Abstract Regular Model Checking
Chalk, Matěj ; Rogalewicz, Adam (referee) ; Hruška, Martin (advisor)
Formal verification methods offer a large potential to provide automated software correctness checking (based on sound mathematical roots), which is of vital importance. One such technique is abstract regular model checking, which encodes sets of reachable configurations and one-step transitions between them using finite automata and transducers, respectively. Though this method addresses problems that are undecidable in general, it facilitates termination in many practical cases, while also significantly reducing the state space explosion problem. This is achieved by accelerating the computation of reachability sets using incrementally refinable abstractions, while eliminating spurious counterexamples caused by overapproximation using a counterexample-guided abstraction refinement technique. The aim of this thesis is to create a well designed tool for abstract regular model checking, which has so far only been implemented in prototypes. The new tool will model systems using symbolic automata and transducers instead of their (less concise) classic alternatives.
|
|
|
A Web Interface for the Management of Virtual Portfolio
Bali, Filip ; Hruška, Martin (referee) ; Lengál, Ondřej (advisor)
This thesis designs and implements a web application for managing virtual portfolios. Main goal of the application is visualise and analyze data from stock exchange services API. User can be notified on price change. The application also uses existing methods to predict stock prices and supports the visualization of the user's stock exchange decisions and provides him/her a general overview of them.
|
|
|
Library for Finite Automata and Transducers
Bieliková, Michaela ; Lengál, Ondřej (referee) ; Hruška, Martin (advisor)
Finite state automata are widely used in the field of computer science such as formal verification, system modelling, and natural language processing. However, the models representing the reality are complicated and can be defined upon big alphabets, or even infinite alphabets, and thus contain a lot of transitions. In these cases, using classical finite state automata is not very efficient. Symbolic automata are more concise by employing predicates as transition labels. Finite state transducers also have a wide range of application such as linguistics or formal verification. Symbolic transducers replace classic transition labels with two predicates, one for input symbols and one for output symbols. The goal of this thesis is to design a library for letter and symbolic automata and transducers which will be suitable for fast prototyping.
|
guest ::
RSS feed.