Case Study: Mobile Robots and Surgical Robots

Table of Contents
  1. Obstacle Avoidance for Mobile Robots
  2. Surgical Robots for Skull-base Surgery
  3. Selected Publications

Obstacle Avoidance for Mobile Robots

On provably safe obstacle avoidance for autonomous robotic ground vehicles
Nowadays, robots interact more frequently with a dynamic environment outside limited manufacturing sites and in close proximity with humans. Thus, safety of motion and obstacle avoidance are vital safety features of such robots. We formally study two safety properties of avoiding both stationary and moving obstacles [1]: (i) passive safety, which ensures that no collisions can happen while the robot moves, and (ii) the stronger passive friendly safety in which the robot further maintains sufficient maneuvering distance for obstacles to avoid collision as well. We use hybrid system models and formal verification techniques that describe and formally verify the robot's discrete control decisions along with its continuous, physical motion. Moreover, we formally prove that safety can still be guaranteed despite location and actuator uncertainty.

Surgical Robots for Skull-base Surgery

Certifying the safe design of a virtual fixture control algorithm for a surgical robotRobotics Business Review
We applied quantified differential-dynamic logic (QdL) to analyze a control algorithm designed to provide directional force feedback for a surgical robot [2]. 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.

Selected Publications

Also see publications on verification of automotive systems.

  1. Stefan Mitsch, Khalil Ghorbal and André Platzer.
    On provably safe obstacle avoidance for autonomous robotic ground vehicles.
    In Paul Newman, Dieter Fox, and David Hsu, editors, Robotics: Science and Systems, 2013.
    [bib | pdf | slides | study | eprint | talk | abstract]

  2. Yanni Kouskoulas, David W. Renshaw, André Platzer and Peter Kazanzides.
    Certifying the safe design of a virtual fixture control algorithm for a surgical robot.
    In Calin Belta and Franjo Ivancic, editors, Hybrid Systems: Computation and Control (part of CPS Week 2013), HSCC'13, Philadelphia, PA, USA, April 8-13, 2013, pages 263-272. ACM, 2013. © ACM
    [bib | pdf | doi | study | abstract]