|
| |
|
|
Analysis of the Impact of Problem Solving Strategies using UPPAAL STRATEGO
Karásek, Filip ; Žádník, Martin (referee) ; Strnadel, Josef (advisor)
This thesis analyzes and addresses the impact of strategies created using Uppaal Stratego. The implementation of four problems, counter, maze, bitmap, and intersection is demonstrated in this thesis. Experiments are conducted on these models, and strategies are formulated. For the first three problems, strategies with a positive impact on the given system were identified. However, for the last intersection model, it was not possible to find a strategy that demonstrably improved the system. This inability to demonstrate improvement is due to limitations in Uppaal Stratego and the complexity of the model.
|
|
|
Statistical Model Checking of Approximate Computing Systems
Blažek, Michal ; Sekanina, Lukáš (referee) ; Strnadel, Josef (advisor)
This bachelor's thesis focuses on the simulation of models of approximate multipliers. The main aim of the thesis is comparing selected properties of multipliers in an application-specific scope of input values. The thesis includes the conversion of multiplier models from the EvoApproxLib library into models used in the UPPAAL environment. These models are then simulated while monitoring their selected evaluation metrics such as error probability, mean absolute error, etc. From the obtained results, one can conclude that using a suitable approximate multiplier in a specific context can have a positive effect on the error in calculations. The results could therefore have further applications in the field of approximate computing systems.
|
|
|
Analysis of Characteristics of Train Traffic Controlled by ERTMS/ETCS
Ondroušek, Adam ; Šimek, Václav (referee) ; Strnadel, Josef (advisor)
The aim of this thesis is to analyze train operations controlled by ERTMS/ETCS, primarily within the Czech Republic. A model was created using the Uppaal software, which simulates train operations. Subsequently, a scenario was designed that significantly increased the efficiency of the modeled track. This scenario was verified using Uppaal SMC's simulation and probabilistic queries. Favourable results were achieved by doubling the intervals of passenger transport during peak hours and adding a freight train unit to the operation during this time with minimal time delay while maintaining operational safety. The model is designed to simulate any train unit and track section and could thus serve as a tool for planning and analyzing train transport after the implementation of ERTMS/ETCS.
|
|
|
Multi-Platform Tool for Generation of Technical Documentation from XML
Jánošíková, Simona ; Setinský, Jiří (referee) ; Strnadel, Josef (advisor)
This bachelor's thesis deals with the challenge in the field of technical documentation of development environments and explores the possibilities of automated generation of documentation from structured XML data. The problem lies in the need for efficient creation and maintenance of technical project documentation through an automated process. The goal of the work is to design, implement and evaluate a multi-platform tool that will be able to generate technical documentation from XML inputs with an emphasis on practical usability in real projects. The work is useful for developers who are involved in the creation and maintenance of technical documentation of development environments. It provides a specific tool that can streamline the documentation generation process and improve the readability of documentation within projects using the XML format for storing information.
|
|
|
Schedulability Analysis of Real-Time Tasks under Uncertainty
Čus, Samuel ; Šimek, Václav (referee) ; Strnadel, Josef (advisor)
The goal of this bachelor’s thesis is to familiarize with real-time systems, uncertainties and scheduling mechanisms related to these systems, statistical model checking, as well as the design and implementation of an approach to schedulability analysis under uncertainties, creating suitable sets of real-time tasks, and verifying their schedulability using the approach. I have mainly incorporated uncertainties caused by system interruptions and undeterministic task parameters. To address the given problem, I created a set of tasks, incorporated uncertainties into the system, and analyzed the schedulability of the tasks. The system modeling and analysis were conducted using the UPPAAL SMC tool, and, for comparison, also using the Cheddar tool with selected sets of tasks.
|
|
|
Dependability Assessment of Fault Tolerant Systems
Suchánek, Martin ; Šimek, Václav (referee) ; Strnadel, Josef (advisor)
Reliability is an important part of various systems. The aim of the work is to create reliability models of some reconfigurable and nonreconfigurable fault tolerant systems and subsequent evaluation of their reliability indicators. The Uppaal tool is used to create models, along with the SMC extension, which is used for verification. The result of the work is the verification of models and evaluation of reliability indicators using the tool Uppaal SMC.
|
|
|
Conversion of XTR Output of UPPAAL Tool into User-Friendly Representation
Mazánek, Antonín ; Mrázek, Vojtěch (referee) ; Strnadel, Josef (advisor)
The master's thesis introduces the Uppaal tool. It describes the principles and possibilities of modeling and analysis of systems using this tool. It also discusses in more detail the file formats that Uppaal tool uses. The structure of the XML file used to store created systems, the XTR format, which Uppaal uses to store simulation traces, and the IF format, which is necessary to understand the contents of the file in XTR format. The text also mentions available software support for working with these formats. Next part of this master's thesis is about designing user-friendly representation of simulations traces, along with designing application that translates simulation traces into designed representation. At the end of this thesis, the possible continuation of the project is mentioned together with the evaluation of the designed representation and the application.
|
|
|
ESP/ESC Impact to Behavior of Vehicle
Weigel, Filip ; Mrázek, Vojtěch (referee) ; Strnadel, Josef (advisor)
This bachelor thesis focuses on active safety - ESP. System ESP greatly improves stability of vehicle while turning. The thesis analyses modelling, brake functionality, subordinate systems of ESP - ABS and ASR, physical forces and phenomenons, model example, analysis of problem, design of model, implementation of model and experiments evaluation of implemented model in UPPAAL enviroment. The goal of the thesis is to prove that ESP system helps to stabilize vehicle while turning by simulation of vehicle model. Results are presented in well-aranged graphs side-by-side. It is possible to analyze the behaviour of vehicle while turning with ESP or without ESP.
|
|
| |
guest ::
