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

• 作者: 关永 孙浩然 施智平 王瑞
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: 混成系统 医疗机器人 微分动态逻辑 微分不变式 形式化验证
• 年，卷（期）: 2018,（18）
• 所属期刊栏目: 工程与应用
• 页码范围: 263-270
• 页数: 8页
• 分类号: TP301.2
• 字数: 7823字
• 语种: 中文
• DOI: 10.3778/j.issn.1002-8331.1705-0343

摘要

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