| Abstract [eng] |
Adaptive computer systems are complex device structures capable of recognizing and accordingly adapting to environmental changes or work disturbances. Computer systems are formally verified; their correctness in relation to the formulated requirements is proven by applying formal mathematical methods. The purpose of this work is to formally verify the adaptive robot cleaning computer-based system using the UPPAAL formal modelling language and associated tool by applying the model checking method, comparing different system configurations by changing the system parameters and its properties, and specifying the system requirements. The analysed system consists of four types of robots, two internal mechanisms of the system, and a process simulating failures. The study proposes a hybrid type of system architecture that combines two widely used strategies, hierarchical and self-organizing, and defines the requirements applied to the system. In the experiments, both classic and statistical (based on simulation and probabilistic evaluation of property satisfaction) model checking methods are applied. Based on the research results, accumulated observations and recommendations for the development of the analysed system and further research are presented. |
