Re: [Paparazzi-devel] Source code analysis of paparazzi

[Matthieu Lemerre]

Hi Karoly,

Karoly Molnar <address@hidden> writes:

>
> Do you mean that you would execute the formal verification of the
> paparazzi code base? It would propel the code quality of this
> autopilot well above any other available autopilot solutions!

Yes. More precisely, the analysis is done using the abstract
interpretation plugin of Frama-C, and the only properties checked are
absence of runtime errors/undefined behaviour in the C code.

This analysis is whole-program (i.e. starts from main() and analyses
every subfunction recursively). By the way, by the look I had to the
code, it seems that the generated source code is single-threaded, but
are there other threads?

At the end of the analysis, I get a list of alarms, which is the list of
statements where a runtime error can possibly occur, meaning that there
are no possible runtime errors that can occur on other statements
(provided we did not make wrong assumptions about the code, such as the
single-threaded hypothesis above). We probably won't be able to reduce
the number down to 0 alarms, but hopefully we would get a low enough
number that the remaining alarms can be checked by hand.

> I have checked Frama-C some times ago and think it is a very promising
> approach. I am just wondering if you would make the analysis framework
> available including all artifacts that would make then possible to
> repeat the analysis?  

I would certainly make sense; I'll see what I can do about this. The
artifacts for now mostly consists in a Makefile that parses the whole
source code of the application (which I manually converted from the
ap_srcs.list file) and options to pass to the value analysis.

> Do you plan to analyze the complete embedded code base including
> libopencm3? I do know that the latter is full of static analysis
> issues so it is very likely that you will detect many during the
> formal verification.

I should be. Are you aware of what specific issues there are in
libopencm3? Also, does Booz2 or Microjet uses libopencm3? It seems to me
that the main function Booz2 never calls any function in libopencm3, but
I might have done something wrong.

Regards
Matthieu