An Assertion Framework for Mobile Robotic Programming with Spatial Reasoning

Assertions are intensively used to facilitate correctness reasoning and error detection in daily programming. However, composing assertions for mobile robotic programs can be painfully inconvenient, because classic Hoare logic lacks the expressing power on spatial knowledge, which is crucial when robots interact with their physical environments. The problem is especially evident for Behavior-Based Robotics (BBR) where the world is not explicitly represented with program variables. In this paper, we propose to incorporate spatial reasoning capability in the assertion framework of Hoare logic. The proposed framework features a two-dimensional region calculus and additional axioms for robot movements. The calculus makes the world representation and the specification of mobile robotic program natural and intuitive, and the axioms enable the reasoning about program correctness. We illustrate the use of the framework with a typical behavior-based robotic program. In addition, we present a runtime error detection and recovery mechanism for BBR programs based on the assertion framework. Preliminary experiments with NAO robots demonstrate the effectiveness.