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.