Researchers Piotr Trojanek and Kerstin Eder from University of Bristol have worked since 2012 on re-implementing well-known navigation algorithms for robots in SPARK, and on verifying that this implementation is free from run-time errors. They publish the results of their work in the major robotics conference IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS 2014) this coming September. See their article attached.

The correctness of robot software is certainly a challenging issue, one on which NASA has been working on for many years for its Mars rovers. As G.J. Holzmann from NASA JPL explains in the February issue of CACM, the C code of Mars rovers has been the subject of 3 types of analyses to eliminate possible run-time errors:

• coding standard checking based on an extension to MISRA C rules
• static analysis with 4 different tools
• model checking focused on the absence of race conditions

But even with this strict process and that many tools involved (completed with tests and code reviews), Holzmann does not claim the code is completely free from run-time errors. It should not be too far though, but certainly the size of the code ("a few million lines of code" as mentioned in the article) and the fact it is written in C make it specially difficult to give guarantees.

Trojanek and Eder targetted much smaller software (around 1 kloc for each of the three algorithms) but they aimed at verifying automatically the absence of run-time errors in the code. This means in particular that, although their software was in C like the NASA code, they could not use the same static analysis tools, which do not report all possible problems (they are not complete) or may over-simplify the true program semantics (they are not sound). They tried instead several state-of-the-art tools for C/C++, but their assessment is that "none of these tools is suitable for automated verification of real-world robot control software, at least not without substantial effort in annotating the source code".

So they turned to SPARK as a means to get effective automated verification. The section II of their paper describes how SPARK features helped them express software specifications succinctly, compared to what would have been required for doing the same on the C version: "[The design of SPARK] greatly reduces the number of explicit annotations required to specify the externally visible behaviour of subprograms - only the essential information needs to be expressed explicitly". This finding echoes a similar one by researchers Christophe Garion and Jérôme Hugues, who have proved the absence of run-time errors in the C/SPARK code of a run-time library for AADL, using tool Frama-C on the C version of the library, and tool GNATprove on the SPARK version of the library. As seen from the conclusions of their experiment (see slides 30, 33 and 34), the weaker semantics of C requires more complex annotations for proof, and results in more work (there are two times more Verification Conditions to prove for the C variant).

In Trojanek and Eder's work, the richer types in Ada compared to C were particularly useful, both for numeric types ("we captured most of the required information using types that constrains the ranges of numeric variables") and record types (using discriminated records to store optional results).

Interestingly, as their SPARK implementation was a direct translation of the three original C programs, the errors they found in the SPARK implementation were also errors in the widely used C versions. They discovered all of these errors simply by testing, using the same simulation environment used with the C programs. The difference with SPARK (and Ada in general) was that the checks executed at run time detected that the program was wrongly "calling mathematical functions with arguments out of their domains" and "accessing an array element at index -1"..

The proof of the 3 SPARK programs did not reveal other errors, but it uncovered hidden assumptions between algorithm parameters, a usual benefit of doing proof. AoRTE was completely proved for one algorithm (SND), requiring manual inspection for only a few unproved Verification Conditions. AoRTE was partially proved automatically for the two other algorithms (94% for VFH+ and 90% for ND). The authors say that proving the remaining checks will require both the user to write additional preconditions and support for invariants in SPARK. Overall, their work is a great demonstration of the strengths of SPARK for developing critical robot software. It also shows where some improvements are needed in the tools to achieve more automation, for example to target true floating-point semantics (in the paper, the researchers assumed real semantics) and to deal with trigonometric functions.

To allow others to extend their work, or to use it as a source of inspiration, Trojanek and Eder have put all their code online at https://github.com/riveras/spark-navigation. Their code is also a very good example of how to use advanced features of SPARK like the formal containers libraryand external axiomatizations. This could be the basis for a library of robotics algorithms in SPARK proved free of run-time errors! I think SPARKY would appreciate.