Národní úložiště šedé literatury Nalezeno 79 záznamů.  1 - 10dalšíkonec  přejít na záznam: Hledání trvalo 0.01 vteřin. 
Petri nets in Netlab Tool
Šajdík, Ondrej ; Smrčka, Aleš (oponent) ; Rogalewicz, Adam (vedoucí práce)
The aim of this work is to support the continuation of the Netlab tool's development and to simplify its extension. Netlab is a desktop application that allows for the modeling of systems in the form of Petri nets using a graphical editor, and subsequently performs model checking analyses on the created model. Within the scope of this work, the concepts of model checking, Petri nets, and available analyses within the application were examined. The application had not been developed for an extended period, resulting in significant obstacles for further improvements. These issues are addressed and resolved throughout the course of this work. Another goal is to enable users of the application to execute a reverse analysis algorithm on the created model, which has been implemented, thereby demonstrating extensibility and potential for future development.
Analýza výkonu programů v jazyce C#
Hájek, Vojtěch ; Rogalewicz, Adam (oponent) ; Pavela, Jiří (vedoucí práce)
Cílem této práce je rozšířit výkonnostní verzovací systém – Perun implementací modulu pro profilování programů napsaných v jazyce C#. Toto rozšíření implementuje profiler s technikou sledování událostí, které jsou získávány pomocí .NET runtime profilovacího aplikačního rozhraní. Profiler dokáže sbírat metriky o sledování funkcí a spotřebě paměti. Naměřené profily potom dokáže dále interpretovat do grafů jako je korelační diagram nebo mapa stromu volání.
Pokročilá statická analýza výkonnosti v nástroji Meta Infer
Pavela, Ondřej ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Looper is a static complexity analysis tool for inference of tight upper bounds on the exe- cution cost of programs. It is based on the previously existing Loopus tool which used abstract program model of difference constraints (inequalities of the form + ), which allows for natural abstraction of common loop counter updates = + + and = + 0. Looper was initially proposed and implemented in author’s bachelor’s thesis as a checker for the Meta Infer framework but the tool failed to meet the expectations when tested on real-world code. This master’s thesis proposes a new improved version of Looper that aims at solving the main limitations of the original tool, namely through introduction of interprocedural analysis. Additionally, various extensions target- ing improved precision of the intraprocedural analysis, such as new abstraction algorithm, handling of compound loop conditions and more, were implemented. Moreover, logging, issue reporting and collection of results has been significantly improved. Finally, through extensive experiments with the new Looper version, the ability to analyze real-world code in a more general, scalable and precise way was shown.
Simulované vkládání chyb v síťové komunikaci
Rozsíval, Michal ; Rogalewicz, Adam (oponent) ; Smrčka, Aleš (vedoucí práce)
Vývoj síťových aplikací probíhá v ideálních podmínkách na rozdíl od jejich nasazení ve skutečném prostředí, které obsahuje chyby jako ztrátovost, zpoždění nebo kybernetické útoky. Zajištění odolnosti proti těmto chybám je tak klíčové. Tato diplomová práce představuje nástroj NetLoiter, jehož cílem je umožnit simulaci požadovaných chyb a umožnit tím vývojářům je správně ošetřit. Nástroj NetLoiter lze použít v transparentní (server proxy), skryté (odchytává komunikaci přímo z jádra systému) nebo hardwarové variantě, která je vhodná například pro testování vestavěných systémů. Nástroj NetLoiter podporuje dynamickou rekonfiguraci pomocí veřejného rozhraní, které je možné využít pro automatizaci procesu testování. Nástroj NetLoiter byl úspěšně integrován a použit v reálných projektech.
Podpora pro prediktivní škálování aplikací na platformě Kubernetes
Fridrich, David ; Pavela, Jiří (oponent) ; Rogalewicz, Adam (vedoucí práce)
Cílem této práce je vytvořit nové rozhraní, které umožní uživateli zpracovávat sbírané metriky pro škálování podle definované formule (např. využití průměrné hodnoty, matematických rovnic, podmíněných příkazů apod.), kterou sám definuje. Dále umožňuje využít externí rozhraní pro připojení komponenty, který definuje vlastní škálovací chování, pomocí kterého může uživatel docílit automatizovaného prediktivního škálování aplikací na platformě Kubernetes. Zvolené problémy jsem vyřešil upravením jádra KEDY implementací nového rozhraní pro škálování podle vlastní formule s aritmetickými a podmiňovacími výrazy a možnosti připojení vlastní externí metody pro výpočet metrik pomocí gRPC technologie. Vytvořené řešení poskytuje flexibilnější způsob zpracovávání metrik a také umožňuje implementovat způsob zcela vlastní
Tool for Searching for Test Paths
Stupar, Michal ; Rogalewicz, Adam (oponent) ; Smrčka, Aleš (vedoucí práce)
The work contains an introduction into problematics model-based testing, framework design for searching test paths over a control-flow graph, the implementation of classes and methods, the implementation of which was verified by a set of automatic tests. Searching path in graphs using breadth-first search and depth-first search algorithms that try to find test paths for performance of the four implemented graph coating criterias. Tool TRIP uses two externals modules - GCC plugin for obtaining the control-flow graph and the SMT solver for determining the evaluation of the path. Communication between moduls is JSON format, which is also used for saving found paths between individual runs of the tool.
A Decision Procedure for Strong-Separation Logic
Dacík, Tomáš ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Separation logic (SL) is one of the most successful tools for verification of programs that manipulate dynamically allocated memory. Its expressive power, however, comes at a cost of undecidability when several of its features are combined, especially separating implications. To circumvent this problem, the recently introduced strong-separation logic (SSL) uses a stricter definition of the semantics, making it decidable, while remaining suitable for verification. However, there is currently no implementation of a decision procedure for SSL. In this work, we propose a decision procedure for SSL based on a translation to first-order formulae that can be later solved by a specialised solver. Our experimental results on restricted fragments where SL and SSL coincide show that our approach can effectively solve formulae obtained from verification tools based on SL and also outperform all other existing translation-based decision procedures. Moreover, during our experiments, we found cases of unsoundness of the heuristics implemented in the decision procedure for SL that is a part of the well-known cvc5 SMT solver. Based on our reports, those heuristics has been fixed.
Single D-Bus Server for SSSD
Úradník, Dušan ; Rogalewicz, Adam (oponent) ; Pavela, Jiří (vedoucí práce)
This thesis aims to reimplement the current topology of SSSD's inter-process communication. This communication is managed through separate D-Bus message buses to which components connect and send messages. The star topology with a single D-Bus requires to create a central message bus for components to use without affecting the current performance of SSSD. To ensure that, a thorough performance analysis had to be done by measuring response times and monitoring SSSD's behavior under constant stream of requests. Therefore, the tools SystemTap and hyperfine were employed to assemble a performance test suite.
Support for Dynamic Config Reload Inside Rsyslog
Lakatos, Attila ; Češka, Milan (oponent) ; Rogalewicz, Adam (vedoucí práce)
Logs are one of the most valuable assets when it comes to IT system management and mon- itoring. As they record every action that took place on a machine, logs provide the insight system administrators need to spot issues that might impact performance, compliance, and security. For this reason, the rsyslog software utility can be used as it offers the ability to accept inputs from a wide variety of sources, transform them, and output the results to diverse destinations by a set of rules. One shortcoming the software currently has is that it needs to be restarted in order to modify the rule set. The author of this master's thesis points out what types of problems a user might encounter during this period of time, such as messages entering the system are lost, TCP/UDP based connections are disturbed, even if no changes are made. The goal of this thesis is to design and implement an option, which allows users to dynamically reload configuration for core components without the need of a full restart. The improvements aim to address problems raised by the research, as well as increase performance by reusing already existing resources.
Asynchronous Task Processing in PCS Project
Pospíšil, Michal ; Pavela, Jiří (oponent) ; Rogalewicz, Adam (vedoucí práce)
The PCS project is a distributed application; therefore, many actions need a way to launch actions in remote application instances. The goal of this thesis is to implement a minimum viable solution for executing actions through a REST API that uses the asynchronous programming model. However, actions themselves are not implemented asynchronously and cannot be invoked directly from asynchronous code. The REST API is connected to an asynchronous scheduler that circumvents this limitation by launching actions in a process pool. The scheduler hides actions behind an abstraction layer of tasks that store information about their status and results. All the actions need to send real-time updates to the clients. This is made possible via a one-way communication channel from the actions to the scheduler that updates the tasks. The REST API provides methods for creating, getting results, and killing tasks. Clients can periodically check the task status and show these updates to the user. Clients can also choose to kill tasks that take too long to finish.

Národní úložiště šedé literatury : Nalezeno 79 záznamů.   1 - 10dalšíkonec  přejít na záznam:
Chcete být upozorněni, pokud se objeví nové záznamy odpovídající tomuto dotazu?
Přihlásit se k odběru RSS.