An Assertion Framework for Mobile Robotic Programming with Spatial Reasoning
2018 IEEE 42nd Annual Computer Software and Applications Conference (COMPSAC)(2018)
摘要
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.
更多查看译文
关键词
assertion framework, Hoare logic, spatial knowledge, error recovery
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络