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 ro...

Full description

Saved in:
Bibliographic Details
Main Authors: Sun, Hao, Ma, Xiaoxing, Dong, Tiansi, Cremers, Armin B., Cao, Chun
Format: Conference Proceeding
Language:English
Subjects:
assertion framework
Calculus
Cognition
error recovery
Hoare logic
Robot programming
Robot sensing systems
spatial knowledge
Task analysis
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0730-3157
DOI:10.1109/COMPSAC.2018.00019