In the course of the last few decades, robotic surgery has become the preferred type of operation within certain types of surgery, allowing the surgeon to perform precision procedures causing the patient a minimal amount of scarring while maintaining an exceptional overview of the operation site for the surgeon.

Advances are made within automation in the control of robotic tools, providing the surgeon with more freedom and higher precision when performing operations. Based on having attended a robotic surgery and recognizing the development within this research community, it is the aim of this thesis to contribute to the advancement through the use of barrier certificates with which safety of the automated control system can be guaranteed.

Control systems are developed for use cases within robotic surgery, including control in 3D Euclidean space and virtual fixture control of a beating heart. System safety is certified through the construction of a barrier enclosing areas termed unsafe thus guaranteeing that the robotic tool will never cross this barrier. Two different approaches are taken: design of safety controllers based on manually constructed control barrier functions, and analytic verification of system safety using a software tool to construct the certificates. The safety verification development constitutes a framework in which any system can be validated in accordance with its safety requirements.

The controllers are implemented in C++ through the ROS framework on a first generation da Vinci surgical robot, and safety is verified for the developed control systems thus demonstrating the applicability of the theory of barrier certificates.