Testing, Verification and Improvements of Timeliness in ROS processes

TL;DR

This paper presents a formal verification approach using Probabilistic Timed Programs and PRISM to improve and verify the response times of ROS-based robotic systems under uncertain processing conditions.

Contribution

It introduces a novel method for verifying real-time behavior in ROS systems through probabilistic formal verification techniques.

Findings

Successful verification of robot response times using PRISM

Identification of potential improvements in robotic operation

Demonstration of probabilistic timeliness analysis in ROS

Abstract

This paper addresses the problem of improving response times of robots implemented in the Robotic Operating System (ROS) using formal verification of computational-time feasibility. In order to verify the real time behaviour of a robot under uncertain signal processing times, methods of formal verification of timeliness properties are proposed for data flows in a ROS-based control system using Probabilistic Timed Programs (PTPs). To calculate the probability of success under certain time limits, and to demonstrate the strength of our approach, a case study is implemented for a robotic agent in terms of operational times verification using the PRISM model checker, which points to possible enhancements to the operation of the robotic agent.