DiNeROS: A Model-Driven Framework for Verifiable ROS Applications with Petri Nets

Verifying industrial robotic systems is a complex task because those systems are often distributed, heterogeneous, and only defined by their implementation instead of models of the system to be verified. Some solutions mitigate parts of this problem, like robotic middlewares such as the Robotic Operating System (ROS), development paradigms such as component-based software engineering, or concrete scientific approaches. However, they all lack the required modeling depth to describe both structure and communication of the system. We introduce a model-driven approach based on Petri nets integrating communication and structural aspects of ROS-based systems. Using a formal modeling language enables verification of the described system and the generation of complete system parts in the form of ROS nodes. This reduces testing effort because the specification of component workflows and interfaces remains formally proven, while only changed implementations have to be revalidated. We evaluate our approach in a case study involving multiple industrial robotic arms and show that the structure of and communication between ROS nodes can be described and verified.