A Formal Model-Based Design Method for Robotic Systems

The model-based approach has been widely applied to the design of software. However, most of these approaches depend on simulation and manual code implementation, which reduces the efficiency and quality of software. In this paper, we present a new model-based approach, which automatically generates the executable C++ code running on the popular Robot Operation System (ROS). Our approach consists of three phases: modeling, verification, and automatic code generation. In the modeling phase, the internal interaction behaviors of robot systems are modeled as a network of timed automata. In the verification phase, the safety requirements are formalized and verified. In the code generation phase, a code generation tool can generate executable C++ code from the verified timed automata model. It bridges the gap between the formal model and the error-prone system implementation. Compared with existing method, the code generator provides the abstractions and mapping of ROS instructions, which realize the seamless connection between the generated code and ROS. The tool also supports most of the complex structures and advanced features of timed automata such as timer, committed location, and synchronous action. For evaluation, a real-industrial robot application of grasping a cup is conducted using our model-based design method, and the generated code can be directly deployed and successfully accomplishes the grasping task.