|
|
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.
|
|
|
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.
|
|
| |
|
|
Intelligent Adaptive Cruise Control of Cars
Smädo, Tomáš ; Šimek, Václav (referee) ; Strnadel, Josef (advisor)
The aim of the bachelor`s thesis is to create a model of intelligent adaptive cruise control system and its surroundings, in which it´s possible to demonstrate its abilities. First, in this thesis we will describe the various types of cruise controls and their sensors. Then we will discuss system modeling fundamentals and utilities for creating such models. Later, in third chapter, we will describe our model design and its implementation. We selected UPPAAL Stratego modeling tool for our implementation. The model in it is created as a network of timed automata. The result of this implementation will be a model of a car with adaptive cruise control with the possibility of switching on this intelligent module and an environment, in which our model will be tested. The model will be tested in the verifier in various scenarios to compare the basic adaptive cruise control functionality with the inteligent cruise control functionality.
|
|
|
Modelling and Analysis of Impacts of ABS to Behavior of Vehicle
Holec, Dominik ; Šimek, Václav (referee) ; Strnadel, Josef (advisor)
Bachelor thesis discusses the ABS braking system and its influence on the braking distance of the vehicle. The thesis includes design, description of the development and testing of the model in the UPPAAL verification environment. The resulting model is a system of intercommunicating timed automata. The analysis of the model properties is based on the method of statistical verification. The model allows us to investigate in particular the course and the length of the braking track. Other variables affecting the behavior of the model that can be tracked are skidding, friction coefficient, air resistance, braking force and vehicle speed. It is also possible to obtain the probability of the vehicle stopping within a certain distance under the chosen conditions and examine the impact of ABS on these results.
|
|
|
Computational Model and Analysis of Self-Driven Vehicle
Gardáš, Milan ; Šimek, Václav (referee) ; Strnadel, Josef (advisor)
This thesis discusses autonomous vehicles. At first it contains describing development of these type of vehicles, how they work and discuss their future development. Further it describe tools which can be used for create model of autonomous vehicle. The thesis includes design, description of the development and testing of the model in the UPPAAL Stratego verification environment. The resulting model is a system of intercommunicating timed automata. The analysis of the model properties is based on the method of statistical verification. The model allows us to investigate behavior of an autonomous vehicle in situations which correspond to regular traffic.
|
|
|
Intelligent Adaptive Cruise Control of Cars
Smädo, Tomáš ; Šimek, Václav (referee) ; Strnadel, Josef (advisor)
The aim of the bachelor`s thesis is to create a model of intelligent adaptive cruise control system and its surroundings, in which it´s possible to demonstrate its abilities. First, in this thesis we will describe the various types of cruise controls and their sensors. Then we will discuss system modeling fundamentals and utilities for creating such models. Later, in third chapter, we will describe our model design and its implementation. We selected UPPAAL Stratego modeling tool for our implementation. The model in it is created as a network of timed automata. The result of this implementation will be a model of a car with adaptive cruise control with the possibility of switching on this intelligent module and an environment, in which our model will be tested. The model will be tested in the verifier in various scenarios to compare the basic adaptive cruise control functionality with the inteligent cruise control functionality.
|
|
|
Computational Model and Analysis of Self-Driven Vehicle
Gardáš, Milan ; Šimek, Václav (referee) ; Strnadel, Josef (advisor)
This thesis discusses autonomous vehicles. At first it contains describing development of these type of vehicles, how they work and discuss their future development. Further it describe tools which can be used for create model of autonomous vehicle. The thesis includes design, description of the development and testing of the model in the UPPAAL Stratego verification environment. The resulting model is a system of intercommunicating timed automata. The analysis of the model properties is based on the method of statistical verification. The model allows us to investigate behavior of an autonomous vehicle in situations which correspond to regular traffic.
|
|
|
Modelling and Analysis of Impacts of ABS to Behavior of Vehicle
Holec, Dominik ; Šimek, Václav (referee) ; Strnadel, Josef (advisor)
Bachelor thesis discusses the ABS braking system and its influence on the braking distance of the vehicle. The thesis includes design, description of the development and testing of the model in the UPPAAL verification environment. The resulting model is a system of intercommunicating timed automata. The analysis of the model properties is based on the method of statistical verification. The model allows us to investigate in particular the course and the length of the braking track. Other variables affecting the behavior of the model that can be tracked are skidding, friction coefficient, air resistance, braking force and vehicle speed. It is also possible to obtain the probability of the vehicle stopping within a certain distance under the chosen conditions and examine the impact of ABS on these results.
|
|
| |
guest ::
