Testing, Verification and Improvements of Timeliness in ROS processes
This work addresses timeliness issues for robotic systems using ROS, but it is incremental as it applies existing formal verification methods to a specific domain.
The paper tackled the problem of improving robot response times in ROS by using formal verification of computational-time feasibility, achieving a method to calculate the probability of success under time limits and demonstrating it with a case study using the PRISM model checker.
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.