Title
Formal Modeling and Automatic Code Synthesis for Robot System
Abstract
Robot control systems are complex cyber-physical systems which are difficult to develop. In this paper, we present a formal model-based automatic code synthesis method which can generate executable C++ code running on the world-wide used Robot Operating System (ROS). The internal interaction behaviors of robot systems are modeled as a network of timed automata. The safety requirements and specifications related to the model are formalized as CTL formulas and verified by Uppaal. We design a code synthesis method to generate the executable C++ code from the verified model. Compared to existing code generators based on timed automata, our method supports more complex structures and advanced features such as timer and committed location, and provides the important abstraction and mapping of ROS instructions, which realize the seamless connection between the generated code and ROS. A case study of grasping a cup by a robot with seven degrees of freedom manipulator is conducted and the generated codes are successfully applied to a ROS development environment.
Year
DOI
Venue
2017
10.1109/ICECCS.2017.17
2017 22nd International Conference on Engineering of Complex Computer Systems (ICECCS)
Keywords
Field
DocType
Formal model,Verification,Automatic code synthesis,Robot system
Robotic systems,Robot control,Programming language,Abstraction,Computer science,Automaton,Real-time computing,Timer,Robot,Code (cryptography),Executable
Conference
ISBN
Citations 
PageRank 
978-1-5386-2432-6
0
0.34
References 
Authors
8
6
Name
Order
Citations
PageRank
Xinxin Li1278.16
R. Wang26111.21
Yu Jiang334656.49
Yong Guan478782.67
Xiaojuan Li5144.14
Xiaoyu Song647151.61