Integrating the Formal Methods part of Qualification

[Andrew.Butterfield at scss.tcd.ie]

Dear RTEMS Developers,

While the validation tests from the RTEMS pre-qualification activity are
now merged into the RTEMS master, the work done in investigating and 
deploying formal methods techniques is not yet merged.

The activity had two main phases: a planning phase (Nov 2018-Oct 2019) 
that explored various formal techniques, followed by an execution phase 
(Oct 2019-Nov 2021) that then applied selected techniques to selected 
parts of RTEMS. Some discussions occurred with the RTEMS community 
via the mailings lists over this time. A short third phase (Nov 2021 - Dec 2021) 
then reported on the outcomes. Each phase resulted in a technical report.

The key decision made was to use Promela/SPIN for test generation, and 
to apply it to the Chains API, the Event Manager, and the SMP scheduler
thread queues. This involved developing models in the Promela language 
and using the SPIN model-checker tool to both check their correctness
and to generate execution scenarios that could be used to generate tests.
Tools were developed using Python 3.8 to support this. Initial documentation 
about tools and how to use them was put into the 2nd phase report.

We now come to the part where we explore the best way to integrate this
into RTEMS. I am proposing to do this under the guidance of Sebastian Huber.

The first suggested step is adding in new documentation to the RTEMS 
Software Engineering manual, as a new Formal Methods chapter. This would 
provide some motivation, as well as a "howto".

I assume that I would initially describe the proposed changes using the patch 
review process described in the section on Preparing and Sending Patches in 
the User Manual.

How do you feel I should best proceed?

Best regards,
  Andrew Butterfield,

--------------------------------------------------------------------
Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
Lero at TCD, Head of Software Foundations & Verification 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/
--------------------------------------------------------------------