spark-navigation

This repository contains implementations of robot navigation algorithms in Ada/SPARK:

• Vector Field Histogram Plus (VFH+)
• Nearness Diagram Navigation (ND)
• Smooth Nearness Diagram Navigation (SND)

The code is already integrated with the Player/Stage robot programming environment and the integration with ROS is planned.

For details of the algorithms, configuration parameters and references, see the list of Player drivers.

Implementations of VFH+ and ND are based on the latest code from the Player repository. Implementation of SND is based on the code from the author's website, as the code is Player repository seems outdated.

For each algorithm there are cpp and ada folders with the original code in C/C++, but including our fixes, and the corresponding code in Ada/SPARK, respectively.

Only the Ada/SPARK implementation of SND has been fully verified for run-time safety (with the assumption that floating-point operations are exact and do not overflow). The other implementations suffer from poor programming style, which prevented us from proving their run-time safety, and/or rely on code features, such as type invariants, that are not yet supported by SPARK.

Compilation

C/C++

The C++ code can be compiled using CMake and the standard procedure for Player driver plugins. The path to the Player installation needs to be set in the individual CMakeLists.txt files.

Ada/SPARK

The code is split into "driver" parts in C++ and full Ada, which integrate the algorithm with the Player, and "algorithm" parts in SPARK, which implement the navigation procedures. The code requires an Ada 2012 compiler and has been developed using GNAT GPL 2013, which can be downloaded from AdaCore.

The navigation algorithms packages depend on the formal numerics package. The two repositories should be downloaded into the same folder.

To build Player plugins use gprbuild -P driver in the ada folders of the individual algorithms. The path to the Player installation needs to be set in the driver.gpr files. The plugins depend on two scenario modes:

• assertions should be set to enable or disable depending on whether the run-time checks should be generated by the Ada compiler,

• numerics should be set to native to use mathematic functions from the Ada standard library or libc to use faster, but less accurate functions from the C standard library.

For example, to build the SND driver with assertions enabled and the native Ada mathematic functions, use gprbuild -P driver -Xassertions=enabled -Xnumerics=native in the snd/ada/ folder.

Verification

To statically verify the "algorithm" code for run-time safety you need a GNATProve with the support for formal containers and formal numerics libraries. For details of the installation process see the formal numerics package README file.

By default, GNATProve uses its own version of the Alt-Ergo SMT solver. An alternative SMT solver that also gives good results is Z3.

Once you are comfortable with the tools, you can:

• check if the code is in the SPARK subset of Ada: gnatprove -P algorithm --mode=check and inspect the algorithm/obj/gnatprove/*.spark files,

• do data-flow analysis: gnatprove -P algorithm --mode=flow,

• prove it: gnatprove -P algorithm --mode=prove --proof=then_split.

Benchmarking

To benchmark the Ada/SPARK code you can use a goto utility. Once the robot reaches the goal location, the drivers prints a message with the number of iterations and the CPU time consumed by the algorithm.

To ease the benchmarking, the driver will shutdown the Player process after reaching the goal location. This behaviour can be disabled by commenting the exit(0) call in the C++ driver code.