Obstacle Avoidance for Mobile Robots
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 [2
]: (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
We applied quantified differential-dynamic logic (QdL) to analyze a control algorithm designed to provide directional force feedback for a surgical robot [1
]. 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.
Also see publications on verification of automotive systems.
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.
[bib | pdf | doi | study