RTEMS qualification and code annotations

Tue Sep 10 13:56:17 UTC 2019

I don't like to top post but in this case I hope this is OK.

This is a very challenging area from a project integration
perspective. There are a handful
of issues which we will have to figure out how to address. I think
these also apply to other
annotations like requirements and licensing annotation

+ Annotation
   - Standards based?
     - For example, will we add annotation for a scanner like Coverity?
   - Invasive/Intruding/Bulk
   - In source file or separate

+ Supporting Tools
   - Free, Libre and Open Source Software
   - Upstream Project not dead
   - Wide Host Support
      - On other cases, have accepted that not all hosts can run the tool

+ Maintenance
  - Availability of Knowledgeable Developers
  - Running Checks as part of Continuous Integration (pre-check ideal)
  - Automated notification of need to update and tracking system

I suggested some guidance in the Software Engineering Guide on broad
tool review
criteria (FLOSS, etc) with a section/chapter on each type of tool we
use (e.g. requirements
for source code control and why git).

I  am pretty sure someone has already used Frama-C on RTEMS. Perhaps
contact the Frama-C
folks and ask. I met one of their core folks at a conference a few
years and he mentioned it.
Perhaps asking their community about this may turn up something.

I'm just trying to make sure we ask all the right questions. Andrew
covered some of them
in great detail.

My first thoughts are:
   - Frama-C seems to be fairly well accepted and meets FLOSS requirement
   - Is ACSL standard?  Supported by anything besides Frama-C?
   -  Annotation needs to be in the source files or it is
unmaintainable IMO. I don't want a
      special tool to merge source. There will end up being annotation
in the source file anyway.
   - Any tool like this has to be part of the currently immature
pre-commit checks and Continuous
     Integration Testing at rtems.org.
   - I don't like that it has issues on other hosts but if the Frama-C
community is willing
     to help address that, it can be worked. I suspect that any of
these special purpose,
     relatively low user base tools will have great cross host support
unless we work with them.

--joel

On Tue, Sep 10, 2019 at 5:45 AM Andrew Butterfield
<Andrew.Butterfield at scss.tcd.ie> wrote:
>
> 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/) 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/
> --------------------------------------------------------------------
>
> _______________________________________________
> devel mailing list
> devel at rtems.org
> http://lists.rtems.org/mailman/listinfo/devel