Formal verification of robotic surgery tasks by reachability analysis