Formal Probabilistic Analysis of a Virtual Fixture Control Algorithm for a Surgical Robot

With the ever-growing interest in the usage of minimally-invasive surgery, surgical robots are also being extensively used in the operation theaters. Given the safety-critical nature of these surgeries, ensuring the accuracy and safety of the control algorithms of these surgical robots is an absolute requirement. However, traditionally these algorithms have been analyzed using simulations and testing methods, which provide in-complete and approximate analysis results due to their inherent sampling-based nature. We propose to use probabilistic model checking, which is a formal verification method for quantitative analysis of systems, to verify the control algorithms of surgical robots. The paper provides a formal analysis of a virtual fixture control algorithm, implemented in a neuro-surgical robot, using the PRISM model checker. We have been able to verify some probabilistic properties about the out-of-boundary problem for the given algorithm and found some new insights, which were not gained in a previous attempt of using formal methods in the same context. For validation, we have also done some experiments by running the considered algorithm on the Al-Zahrawi surgical robot.