Safety Verification of Industrial Robotic Systems

Verification methods commonly used for robotic systems, such as simulation and manual testing, may be insufficient as they cannot evaluate all possible scenarios. Therefore, formal methods have been developed for safety verification. Model-based formal methods can supervise all system states and possible state transitions. However, the challenges of model creation and verification hinder the adoption of these techniques by developers of robotic systems. This study proposes a method to facilitate the modeling and verification of robotic system software. In the proposed method, the behavioral aspects of the system software are modeled as timed automata. To alleviate the complexity of these models, components with common functionalities in robotic systems are designed as templates. These templates include timed automata that perform the represented functions. UPPAAL software tool is employed to implement the model checking technique in this study. To demonstrate the feasibility of the proposed method, a production station where multiple industrial robots collaborate is considered.