Formal construction and verification of home service robots: A case study

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.