RTEMS qualification and code annotations

[Andrew Butterfield]

Dear Chris,

  first, thanks for trying to install it ! 

 Frama-C is one of a number of tools we are considering, so it's not a done deal.

 If used, it would only be applied to a small part of the codebase: 
  typically code that is very critical, but hard to test reliably.
 I would expect that this code would be unlikely to change much, if at all.

The contents of the annotations would have to be maintained by those familiar with
the annotation  language(ACSL*) and how it should be used.

They would also be responsible
for ensuring that any loop annotations in .c files would be revised if there was any significant
code refactoring that altered the number or purpose of those loops.

The annotation in the .h files capture  the specification of what the code should do,
as pre/post-condition pairs - once setup and validated, they shouldn't change much.

Frama-C has two main components: 
 ` frama-c`  :  a command line tool that does all the work, and is highly automatable
  `frama-c-gui` : a nice GUI that interacts with `frama-c`, and produces verification results
    that can be re-run from the command line.

The plan is that the GUI might be used to develop/debug/validate the various annotations,
but that the day-to-day use of Frama-C as part of the qualification toolset would simply
involve re-running the verifications using the command-line tool, all automated. It would
only be if this reported some verification failure that any action would need to be taken.
This would mean that only the command-line tool would need to be installed, which might
reduce the package count somewhat.

A quick potted history of Frama-C was that it was developed, starting in 2010,
by CEA (http://www-list.cea.fr/en/ <http://www-list.cea.fr/en/>) on top of a previous tool called CAVEAT they had
that was used internally by Airbus. It was designed specifically to automate formal
verification of  Airbus C code, and then made available to the community at large.

An issue with it is that it handles C99, but not C11, which may be a show-stopper for us.

 Regards, Andrew

* ACSL = "ANSI C Specification Language"



> On 10 Sep 2019, at 02:36, Chris Johns <chrisj at rtems.org> wrote:
> 
> On 6/9/19 9:40 pm, Andrew Butterfield wrote:
>> However, if the implementation code contains loops, then we need annotations in
>> the code at those loops. The following, from the Frama-C ACSL Tutorial
>> (https://frama-c.com/acsl_tutorial_index.html) shows the annotations required to
>> verify the correctness of a function that finds the maximum of a sequence of
>> integers.
> 
> Am I to assume Frama-C is the analysis tool for this work?
> 
> I have taken a look at this tool however it would be nice to get some
> understanding of its history and how you see it fitting in to the RTEMS project
> and how we as a project take these annotations and maintained them.
> 
> I see on the Frama-C website Linux is supported and so I decided see how FreeBSD
> goes. I installed ocaml for FreeBSD as a result of some configure errors with ..
> 
> $ pkg install ocaml ocaml-findlib
> 
> however configure returned ...
> 
> checking for ocamlgraph... ocamlfind: Package `ocamlgraph' not found
> 
> This one package wants to install 118 packages some dependent on gnome,
> gnome-theme, docbook, gstreamer, bash and more so I have said no to installing
> them and I have decided to give up for now. The box I am using is a headless
> build server.
> 
> Chris

--------------------------------------------------------------------
Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
Lero at TCD, Head of Foundations & Methods Research Group
School of Computer Science and Statistics,
Room G.39, O'Reilly Institute, Trinity College, University of Dublin
                         http://www.scss.tcd.ie/Andrew.Butterfield/
--------------------------------------------------------------------

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.rtems.org/pipermail/devel/attachments/20190910/c738f133/attachment-0002.html>