|
|
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.
|
|
|
Autonomous Control of Cars
Čurda, Vojtěch ; Bidlo, Michal (referee) ; Strnadel, Josef (advisor)
The purpose of this bachelor's thesis is to create a model of a self-driving vehicle, along with its surroundings. At first, the thesis outlines the vehicle automation and the system modeling problematics. The thesis then shows the design of said model, as well as its implementation. The model was implemented in UPPAAL Stratego - a tool that is used for modeling, validation and verification of real-time systems, in which the model is implemented as networks of timed automata. The result is a model of a self-driving vehicle, that can drive itself on a motorway with an arbitrary amount of traffic lanes. The self-driving vehicle reacts appropriately to the movement of other vehicles on the motorway and can change its speed according to speed limiting traffic signs. The behaviour of the model is then validated with the help of statistical analysis, which is done using the verification language embedded in the mentioned tool. The model is tested in specific scenarios, as well as random scenarios, where the self-driving vehicle is set into a 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.
|
|
|
Search of Control Strategies Using UPPAAL STRATEGO
Hruška, Filip ; Hrubý, Martin (referee) ; Strnadel, Josef (advisor)
This thesis deals with finding control strategies for pre-selected problems from various areas using tool Uppaal Stratego. Four areas were selected, namely chess, a sliding puzzle, the tower of Hanoi, and a kinematic problem involving a package, a car, and an airplane. For the selected areas and problems, a set of models was designed and implemented. For the tower of Hanoi and the sliding field, it was possible to successfully evaluate relevant strategies, raising the probabilities of success to more than 90 %. For other models, a problem was found in the size of the state space and the strategies could not be evaluated because the maximum memory capacity that the tool uses was not sufficient. For the kinematic problem, after limiting and simplifying the model, the strategies were successfully evaluated, but for chess, this was not possible even after significant simplification.
|
|
|
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.
|
|
|
Autonomous Control of Cars
Čurda, Vojtěch ; Bidlo, Michal (referee) ; Strnadel, Josef (advisor)
The purpose of this bachelor's thesis is to create a model of a self-driving vehicle, along with its surroundings. At first, the thesis outlines the vehicle automation and the system modeling problematics. The thesis then shows the design of said model, as well as its implementation. The model was implemented in UPPAAL Stratego - a tool that is used for modeling, validation and verification of real-time systems, in which the model is implemented as networks of timed automata. The result is a model of a self-driving vehicle, that can drive itself on a motorway with an arbitrary amount of traffic lanes. The self-driving vehicle reacts appropriately to the movement of other vehicles on the motorway and can change its speed according to speed limiting traffic signs. The behaviour of the model is then validated with the help of statistical analysis, which is done using the verification language embedded in the mentioned tool. The model is tested in specific scenarios, as well as random scenarios, where the self-driving vehicle is set into a regular traffic.
|
|
|
Search of Control Strategies Using UPPAAL STRATEGO
Hruška, Filip ; Hrubý, Martin (referee) ; Strnadel, Josef (advisor)
This thesis deals with finding control strategies for pre-selected problems from various areas using tool Uppaal Stratego. Four areas were selected, namely chess, a sliding puzzle, the tower of Hanoi, and a kinematic problem involving a package, a car, and an airplane. For the selected areas and problems, a set of models was designed and implemented. For the tower of Hanoi and the sliding field, it was possible to successfully evaluate relevant strategies, raising the probabilities of success to more than 90 %. For other models, a problem was found in the size of the state space and the strategies could not be evaluated because the maximum memory capacity that the tool uses was not sufficient. For the kinematic problem, after limiting and simplifying the model, the strategies were successfully evaluated, but for chess, this was not possible even after significant simplification.
|
|
|
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.
|
guest ::
