Formally verifying navigation safety for ground robots

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

5 Scopus citations

Abstract

Robots' continuous physical behaviors are controlled by discrete instructions generated using complicated control algorithms. In such a robotic hybrid system, guaranteeing robot's navigation safety can be more challenging than those discrete controls alone or only the continuous robot motions. For a robotic system operating in the real world, navigation safety is critical in order to avoid potential harm for robots or their surrounding environment. We present safety guarantee and obstacle avoidance control algorithms for mobile ground robots modeled by hybrid programs. Using the verification tool KeYmaera, we formally verify that our algorithms satisfy passive or passive friendly safety properties in an environment consisting of stationary/dynamic obstacles. These algorithms allow us to check the navigation safety at the design stage of a robotic system.

Original languageEnglish
Title of host publication2016 IEEE International Conference on Mechatronics and Automation, IEEE ICMA 2016
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages1000-1005
Number of pages6
ISBN (Electronic)9781509023943
DOIs
StatePublished - 1 Sep 2016
Event13th IEEE International Conference on Mechatronics and Automation, IEEE ICMA 2016 - Harbin, Heilongjiang, China
Duration: 7 Aug 201610 Aug 2016

Publication series

Name2016 IEEE International Conference on Mechatronics and Automation, IEEE ICMA 2016

Conference

Conference13th IEEE International Conference on Mechatronics and Automation, IEEE ICMA 2016
Country/TerritoryChina
CityHarbin, Heilongjiang
Period7/08/1610/08/16

Keywords

  • collision avoidance
  • formal methods
  • mobile ground robot
  • motion safety

Fingerprint

Dive into the research topics of 'Formally verifying navigation safety for ground robots'. Together they form a unique fingerprint.

Cite this