文献类型：期刊文章

作　　者：孙浩然[1,2] 施智平[1,2,3] 关永[1,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

出　　处：《计算机工程与应用》

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

年　　份：2018

卷　　号：54

期　　号：18

起止页码：263-270

语　　种：中文

收录情况：AJ、BDHX、BDHX2017、CSA、CSA-PROQEUST、CSCD、CSCD_E2017_2018、IC、INSPEC、JST、RCCSE、ZGKJHX、核心刊

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

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

分 类 号：TP301.2]