Formal Verification of ROS Based Systems Using a Linear Logic Theorem Prover

Abstract

In this paper, we propose a novel representation and verification technique for software components in a robotic system using a linear logic theorem prover. Linear logic includes consumable resources together with persistent resources, enabling representing and reasoning of robotic domains. We demonstrate model representation and verification of formal specifications through Robot Operating System (ROS) components. The system model can be either statically extracted by HAROS (a ROS based static analysis framework) or dynamically extracted once all system components are running. After ten years of its first release, ROS has become one of the most popular middlewares among robotic programming frameworks. Even though ROS is very popular among robotic developers, we believe that a framework for easily representing and verifying robotic systems is missing. This paper introduces a new technique for formally representing and verifying robotic systems using a linear logic theorem prover and finally presents a number of illustrations of model representation and safety property checking both statically and dynamically for the robot Kobuki.