Safety verification of industrial robotic systems

In this master's study, security problems and security verifications arising from the interaction of robotic systems with the environment and with each other are discussed. Safety in robotic systems is an area where comprehensive and satisfactory results should be obtained. For robotic systems, it is necessary to provide security according to certain conditions and situations. Traditional methods may be insufficient in the security verification of software developed for robotic systems. For this reason, formal methods have been developed for security verifications. To use formal methods, a specific problem that the robotic system is expected to be tested for is described. The type of formal method to be used in accordance with the defined problem is determined. Within the scope of this study, a problem has been prepared for the use of formal verification methods in robotic systems. In this direction, scenarios were created for different products walking on the conveyor belt to be picked up by robotic arms and transferred to the points where they belong. Model inspection method is used in order to make the most appropriate security verification according to the current problem in the robotic system. In this method, the UPPAAL tool, which provides modeling of real­time systems, is preferred. In this study, scenarios are prepared for the current problem and security verifications are made using the relevant modules in the vehicle. It is seen that similar models are made for similar scenarios in line with the examinations on the models prepared in the UPPAAL tool according to the scenarios. Based on these similarities, a general template was prepared for robotic arm systems with similar scenarios and it was revealed whether it is applicable when creating different models. The use of the UPPAAL tool and the security validation of the models are included in the scope of this study, while the scenario­based models prepared within the scope of the problem are experimentally demonstrated. Keywords: Model checker, formal verification, robotic systems, safety, timed automatons