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

摘要： 混成系统是实时嵌入式系统的重要子类，其行为中存在连续变化和离散跳转混杂的情况，使得混成系统行为复杂，安全性难以掌握。近年来，混成系统在医疗环境中得到越来越广泛的应用。其中，医疗机器人的穿刺运动控制系统呈现高度复杂的混成性，如果机器人在穿刺过程中失控将导致不可挽回的严重后果。因此穿刺机器人运动行为的安全性设计成为了亟需解决的问题。首先根据穿刺机器人的运动学设计，将机器人的复杂运动分解。然后基于微分动态逻辑理论从混成系统的角度出发对穿刺机器人的运动控制系统进行了形式化建模与分析，并使用证明工具KeYmaera归纳出微分不变式，获得了控制模型的参数约束。最后提出了针对机器人运动到某一靶目标区域这类运动学问题的一般性验证模型。

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