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

来源：计算机工程与应用杂志2018年第18期北京时间：

作者：孙浩然1，2，施智平1，2，3，关 永1，3，王 瑞2，3

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

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

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