Formal Modeling and Automatic Code Synthesis for Robot System

• DOI: 10.1109/iceccs.2017.17
• Publication Date: 2018-02-15T16:32:24Z
• Authors: Xinxin Li; Rui Wang; Yu Jiang; Yong Guan; Xiaojuan Li; Xiaoyu Song
• Keywords: Executable; Code (set theory); Abstraction

Robot control systems are complex cyber-physical which difficult to develop. In this paper, we present a formal model-based automatic code synthesis method can generate executable C++ running on the world-wide used Operating System (ROS). The internal interaction behaviors of robot modeled as network timed automata. safety requirements and specifications related model formalized CTL formulas verified by Uppaal. We design from model. Compared existing generators based automata, our supports more structures advanced features such timer committed location, provides important abstraction mapping ROS instructions, realize seamless connection between generated ROS. A case study grasping cup with seven degrees freedom manipulator is conducted codes successfully applied development environment.