Formal Verification of Robot Movements - a Case Study on Home Service Robot SHR100

Home service robots have received much attention from both academia and industry because home service robots have wide range of potential applications such as home security, cleaning, etc. The robots need to add or update services frequently according to the changing needs of human users. Furthermore, reactive nature of the robots add complexity to develop robot applications. These challenges raise safety issues seriously. Considering that safe operation of home service robots is crucial, current practice of validating robot applications is, however, not mature enough for wide deployment of home service robots. In this paper, we present our experience of developing and formally verifying discrete control software of Samsung Home Robot (SHR) using Esterel. We give a brief background on Esterel, then illuminate our result in formally verifying stopping behavior of SHR. Through the verification, we could detect and solve a feature interaction problem which caused the robot not to stop when a user commanded the robot to stop.
Publisher
IEEE
Issue Date
2005-04-18
Language
ENG
Description

Proceedings of the 2005 IEEE International Conference on Robotics and Automation Barcelona, Spain, April 2005

Citation

International Conference on Robotics and Automation, pp.4739 - 4744

ISSN
1050-4729
URI
http://hdl.handle.net/10203/474
Appears in Collection
CS-Conference Papers(학술회의논문)
Files in This Item
01570852.pdf(257.15 kB)Download
  • Hit : 410
  • Download : 397
  • Cited 0 times in thomson ci

qr_code

  • mendeley

    citeulike


rss_1.0 rss_2.0 atom_1.0