Certifying the safe design of a virtual fixture control algorithm for a surgical robot

Abstract

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.