Runtime Verification of Robots Collision Avoidance Case Study

The robot has attracted much attention to anticipate improved quality of human life. Real-time obstacle avoidance is one of hot spots of the research. Runtime verification is a real-time and lightweight verification technology to verify the properties in many fields. In this case study, we use the JavaMOP, a runtime verification tool to verify the implementations' correctness of the safety strategies for avoiding collision as a complement to the design. The design of the safety strategies can be classified as the pre-contact safety strategy and the post-contact safety strategy. The former can avoid obstacles and the latter can reduce the physical damage after a collision. Additionally, this case study also proposes a new method of dynamic parameter selection. It can automatically update the parameters during the operation of the robot without having to get familiar with and to modify robot programs. Because some special parameters may change as mutative factors or be updated by engineers' experience in the uncertain environment, they cannot be fixed. We follow the JavaMOP specification to describe informal requirements using the FSM and ptLTL languages. Finally, the experimental results verify the correctness of the safety strategies and the effectiveness of dynamic parameter selection.