穿刺机器人运动安全性的形式化分析与建模  

Analysis and formal modeling of puncturing robot's sports safety

作　　者：孙浩然 施智平[1,2,3] 关永 王瑞[2,3] SUN Haoran;SHI Zhiping;GUAN Yong;WANG Rui(Sophisticated Imaging Technology Innovation Center,Capital Normal University,Beijing 100048,China;Light Industrial Robot and Safety Verification of Key Laboratory of Beijing,Capital Normal University,Beijing 100048,China;Beijing Mathematics and Information Science 2011 Collaborative Innovation Center,Beijing 100048,China)

机构地区：[1]首都师范大学成像技术北京市高精尖创新中心,北京100048 [2]首都师范大学信息工程学院轻型工业机器人与安全验证北京市重点实验室,北京100048 [3]北京数学与信息交叉科学2011协同创新中心,北京100048

出　　处：《计算机工程与应用》2018年第18期263-270,共8页Computer Engineering and Applications

基　　金：国际科技合作计划(No.2010DFB10930,No.2011DFG13000);国家自然科学基金(No.61170304,No.61104035,No.61373034,No.61303014,No.61472468,No.61572331);北京市科委项目(No.Z141100002014001);北京市教委科研基地建设项目(No.TJSHG201310028014);北京市属高等学校创新团队建设与教师职业发展计划项目(No.NoIDsHT20150507)。

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

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

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]