https://www.mdu.se/

Robotic systems often operate under real-time constraints, requiring timely responses to sensor inputs. Early consideration of such requirements during design is advantageous. The Robot Operating System (ROS) provides a mature framework for system setup and communication, with ROS 2 offering real-time capabilities. However, determining the maximum reaction time within a ROS-based application is intricate due to complex variable processing and scheduling, especially with periodic and event-triggered tasks. In this paper, we propose a model of ROS-based designs with timed automata semantics, facilitating exhaustive real-time model checking of system behavior. We extend this model to stochastic timed automata, thus incorporating non-deterministic execution time and probabilistic loads, employing statistical model checking for scalability and accuracy. We compare against previous work to confirm the validity of our approach, and show its applicability on a real-world robotic system example.