ROBOREBECA: A NEWFRAMEWORK TO DESIGN VERIFIED ROS-BASED ROBOTIC PROGRAMS

Robotic technology helps humans in different areas such as manufacturing, health care and educa-tion. Due to the ubiquitous revolution, today’s focus is on mobile robots and their applications in avariety of cyber-physical systems. There are several powerful robot middlewares, such as ROS andYARP to manage the complexity of robotic software implementation. However, they do not providesupport for assuring important properties such as timeliness and safety. We believe that integratingmodel checking with a robot middleware helps developers design and implement high quality roboticsoftware. By defining a general conceptual model for robotic programs, in this thesis we present anintegration of Timed Rebeca modeling language (and its model checker) with ROS to automaticallysynthesize verified ROS-based robotic software. For this integration, first the conceptual model ismapped to a Timed Rebeca model which is used to verify the desired properties on the model. The Timed Rebeca model may be modified several times until the properties are satisfied. Finally, theverified Timed Rebeca model is translated to a ROS program based on a set of mapping rules. Conducting experiments on some small-scale case studies indicate the usefulness and applicability ofthe proposed integration metho