Certifying the safe design of a virtual fixture control algorithm for a surgical robot
Certifying the safe design of a virtual fixture control algorithm for a surgical robot
复制标题
验证手术机器人虚拟夹具控制算法的安全设计
DOI：
10.1145/2461328.2461369
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
P. Kazanzides
中科院分区：
文献类型：
--
作者：
Yanni Kouskoulas;David W. Renshaw;André Platzer;P. Kazanzides
我们应用量化微分动态逻辑（QdL）分析的控制算法，旨在提供方向力反馈的手术机器人。我们发现了算法的问题，证明了它通常是不安全的，并准确地描述了可能出错的地方。然后，我们应用QdL来指导新算法的开发，该算法沿着定向力反馈提供安全操作。使用\KeYmaeraD（一种机械化QdL的工具），我们创建了一个机器检查的证明，保证新算法对所有可能的输入都是安全的。
We applied quantified differential-dynamic logic (QdL) to analyze a control algorithm designed to provide directional force feedback for a surgical robot. We identified problems with the algorithm, proved that it was in general unsafe, and described exactly what could go wrong. We then applied QdL to guide the development of a new algorithm that provides safe operation along with directional force feedback. Using \KeYmaeraD (a tool that mechanizes QdL), we created a machine-checked proof that guarantees the new algorithm is safe for all possible inputs.