Overview

The resulting approach is illustrated in the figure below.

The user designs a robot behavior using Behavior Trees to orchestrate Skills (as defined in SmartSoft metamodel). Using an automatic tool, such Behavior Tree is compiled into executable code using an execution engine. This engine is generated using the Coq proof assistant starting from the Behavior Tree description and a well-defined operational semantic. The engine is then loaded and executed as a SmartSoft component to orchestrate SmartSoft or YARP components.

We use contracts and contract-based design as a methodology to describe skills and the use of off-the-shelf verification tools NuSMV to statically verify correct execution of the Behavior Tree. To this end the Behavior Tree is translated to a Hierarchical Finite State Machine using an automatic tool.

From the description of the Behavior Tree in terms of Hierarchical Finite State Machine another automatic tool can also generate runtime monitors. Monitors ensure that the properties assumed during the static verification of the Behavior Tree are still valid at runtime, and generate an exception otherwise.

We defined the three scenarios for the experimental validation of the CARVE methodology and tools. The description and the experimental validation are available for Scenario 1, 2, and 3.

Contract-based design

The contract-based design methodology for has been used to validate the three reference scenarios. We defined syntax and operational semantics for Behavior Trees. This allowed us to implement an automatic tool that can generate an execution engine which conforms to the given semantics and that has guaranteed termination.

To support static verification of Behavior Trees we propose contract based design and verification methodology for robotics. This allowed us to verify desirable properties of the overall system model. The system model includes Behavior Tree, the skills it coordinates and the environment. Properties are expressed in temporal logic and verified offline using the NuSMV model checker. The procedure is depicted in the figure below.

Videos showing the execution of the static analysis are in the Media page.

Runtime Monitoring

Runtime monitoring is used to carry out runtime verification, i.e., ensure that during deployment on the real robot everything other than the BT behaves as expected.

Given the abstract models for the skills and the environment, we can verify that at runtime, the skill and the evironment behave as expected. Videos showing the executions of runtime monitors are in the Media page.

Integration with SmartSoft

For the integration of the Behavior Tree execution engine in SmartSoft we developed a dedicated component that can execute the engine. We also implemented the code to achieve interoperability between the SmartSoft toolchain and YARP (the middleware used on the R1 robot).

To achieve better interoperability we also mapped the RobMoSys communication patterns into their YARP equivalent. A video showing this integration is available in the Media page.

Integration with the Mood2Be ITP

We also integrated the Behavior Tree graphical editor developed by the Mood2Be ITP (Groot) so that it can be used to design a Behavior Tree compatible with the CARVE toolchain and visualize the status of the execution engine. The Groot GUI has been used for the development and execution of the Scenario 1, 2, and 3.