Formal construction and verification of home service robots: A case study
SCIE
SCOPUS
- Title
- Formal construction and verification of home service robots: A case study
- Authors
- Kim, M; Kang, KC
- Date Issued
- 2005-01
- Publisher
- SPRINGER-VERLAG BERLIN
- Abstract
- Home service robots have attracted much attentions to anticipate improved quality of human life. Considering that malfunctions of home service robots can directly threat the safety of human users, the assurance of robot's safe operation is a crucial prerequisite for the wide deployment of home service robots. Current practice of robot development, however, often fails to satisfy this requirement. Robot developers tend to concentrate on technical components only and fail to consider how these components will integrate to create the service. This practice frequently causes feature interaction problems. Furthermore, reactive nature of the robot applications adds to further complexity. Traditional testing is unsuccessful with this setting due to the difficulty of testing embedded systems and uncertainty caused by sensor devices. These situations make formal construction and verification essential to ensure safe operation of home service robots. In this paper, we present our experience of formally constructing and verifying the core of Samsung Home Robot (SHR) with the use of Esterel. First, we reverse-engineered SHR to identify and analyze the core of SHR. Then, we re-implemented the core part in Esterel and verified SHR to satisfy safety properties regarding stopping behaviors through model checking. Through the verification, we detected and solved a feature interaction problem which caused the robot to ignore a stop command.
- URI
- https://oasis.postech.ac.kr/handle/2014.oak/24277
- DOI
- 10.1007/11562948_32
- ISSN
- 0302-9743
- Article Type
- Article
- Citation
- LECTURE NOTES IN COMPUTER SCIENCE, vol. 3707, page. 429 - 443, 2005-01
- Files in This Item:
- There are no files associated with this item.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.