Synthesis-based engineering of supervisory controllers for ROS-based applications

An ever-increasing number of robotic applications is being created based on the functionalities and the communication facilities offered by the Robotic Operating System (ROS). When applications involve contact with humans, such as in some transportation tasks, a robot supervisory controller shall guarantee that in every possible circumstance safety and task requirements are satisfied. There is no framework provided by ROS to specify supervisory controllers with formal guarantees about the satisfaction of requirements. This is problematic when the complexity of the controller increases, and it is not viable to test every possible scenario during the validation stage of the robotic application. This paper presents novel work that aims at enabling supervisory controller synthesis for ROS-based applications by (a) proposing a novel mapping between concepts from supervisory control theory and ROS, (b) demonstrating that a supervisory control modeling language exists that can be used to describe plant models and to specify requirements and (c) presenting generic finite-state automata models of ROS components, regarded as plant models, which are input for the synthesis procedure. The approach is demonstrated by synthesizing the controller to coordinate state-of-the-art mobile robot navigation modules. Simulations and real-life experiments show that the generated supervisory controller guarantees the correctness of the model with respect to the requirements and that the execution time of a control loop, including the binding code between the supervisory controller and ROS, is on average short enough to be deployed in high-level control loops. The paper is accompanied by a public code repository that contains the implementation of all methods presented in the paper including simulation environments to ease the replication of the results presented.