Formal Verification Applied to Robotic Surgery