关键词: 混成系统, 医疗机器人, 微分动态逻辑, 微分不变式, 形式化验证

Abstract: Hybrid system is a very important subclass of the real-time embedded system. Discrete control mode transformation and continuous real time behavior are tangled in the behavior of the hybrid system, resulting in complex system behaviors and hard control of safety. In the last few decades, the application of puncturing robots has widely increased in the case of surgery. Thereinto, the control system of surgical robots’ puncturing motion shows a high complex hybrid property. Irretrievable consequences will be made if robots lose control when performing puncture. Therefore, security design for puncturing robots’ behaviors has become an especially urgent problem to solve. Firstly, based on the kinematic design of puncturing robots, the complex motion of the robots is resolved into a simpler one. Then, on the basis of the differential dynamic logic theory, formal modeling and analysis are worked out for several parts of the control system of puncturing robots’ motion from the perspective of hybrid system; a differential invariant is deduced and the parameter constraint of the control system is worked out with assistance of the proof tool KeYmaera. Finally, a generalized formal model is put forward specific to the movement of robots to a certain target region.

Key words: hybrid system, surgical robot, differential dynamic logic, differential invariant, formal verification