Verification of ROS Navigation 2's NavFn planner using Maude and Dafny
The Maude implementations of the NavFn algorithm are in the src/maude
directory. There are various versions:
- NavFnA* is a textbook implementation of the A* algorithm. It can be executed with the
a*
operator of theASTAR
module inastar_textbook.maude
. - NavFnpot calculates a potential function imitating the
NavFn
planner of Navigation 2, and then computes the path from the origin to the goal by always taking the neighbor with the lowest potential as the next position. This is thecomputePath
function of theBASIC-TRAVERSE
module incommon.maude
. - NavFnROS imitates the complete
NavFN
implementation, also in the second phase where the path is computed. It is available in thea*
function of theASTAR
module inastar_navfnplanner.maude
.
The Dafny implementation of the NavFn planner are in the src/dafny
directory.
Some properties are verified using both Dafny (see src/dafny
) and manually-specified verification conditions in Maude (see src/maude/verification
).
The Python-based ROS action server that integrates the planner into the Navigation 2 stack is in the src/maude/integration
directory. The main file, planner_action_server.py
, includes instructions for a dummy simulation.
The Turtlebot 3 simulator can be started with the Maude planner using run_simulation.sh
in an environment similar to that of Dockerfile
.