Integrating the Formal Methods part of Qualification

Wed Jul 6 19:07:33 UTC 2022

On Sun, Jul 3, 2022 at 7:49 PM Chris Johns <chrisj at rtems.org> wrote:
>
> On 2/7/2022 12:59 am, Andrew Butterfield wrote:
> > On 1 Jul 2022, at 00:59, Chris Johns <chrisj at rtems.org
> > <mailto:chrisj at rtems.org>> wrote:
> >>
> >> On 28/6/2022 11:09 pm, Andrew.Butterfield at scss.tcd.ie
> >> <mailto:Andrew.Butterfield at scss.tcd.ie> wrote:
> >>> 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.
> >>
> >> Congratulations for the work and results you and others have managed to achieve.
> >> It is exciting to see this happening with RTEMS and being made public.
> >>
> >>> 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?
> >>
> >> It is hard for me to answer until I understand what is being submitted and who
> >> maintains it? I am sure you understand this due to the specialised nature of the
> >> work.
> >
> > Indeed, I quite agree.  I have some short answers below, with suggestions.
>
> Thanks.
>
+1

> >
> >>
> >> What will be submitted, ie SPIN files, scripts, etc?
> >
> > Promela/SPIN model files (ASCII text, C-like syntax)
> > C template files (.h,.c) to assist test code generation
> > YAML files to provide a mapping from model concepts to RTEMS C test code
> > python scripts to automate the test generation
> > Documentation - largely RTEMS compliant sphinx sources (.rst)
> >
> >>
> >> Where are you looking to add these pieces?
> >
> > Everything except the documentation could live in a top-level folder ('formal')
> > in rtems-central.
> > In fact there is no particular constraint from my perspective for where they can go.
>
> Using rtems-central is fine.
>
Do they require anything currently located in rtems-central? Are the
models or YAML files related to the current specification files? I
know I'm guilty of not spending the time yet to deeply learn
rtems-central, but I would like to know that these files will fit
within that repo as it currently is intended to operate.

RSB should be taught how to build the necessary host tools to run Promela/SPIN.

> > The plan would be to add the pertinent parts of our project documentation into
> > new chapters
> > in the RTEMS software engineering manual. So that would be eng/ in the
> > rtems-docs repo.
>
> Great.
>
+1

A new section in the eng should be suitable. I would actually
recommend using
https://docs.rtems.org/branches/master/eng/test-framework.html# as a
good example.

> >> How is the verification run against the code? Do we manage regression testing
> >> and is that even possible?
> >
> > The python scripts basically run SPIN in such a way as to generate scenarios
> > that model
> > correct behaviour which then get turned into standard RTEMS test programs. These all
> > get added into a new testsuite in the rtems repo (testsuites/models, say).
> > They are properly integrated into the RTEMS test system, so get built and run by
> > waf.
> > This is similar to how the tests generated by Sebastian in testsuites/validation
> > are handled.
> >
> > From the perspective of a user that works out of git.rtems.org/rtems
> > <http://git.rtems.org/rtems>,
> > there will be no obvious impact - just some extra tests in among the ones that
> > already exist.
>
> Thanks and this make sense.
>
> >
> >>
> >> I hope my simple questions highlight a lack of understand on how this works and
> >> how we maintain it and use it once integrated.
> >
> > I intend to continue to work and maintain this for the foreseeable future. I
> > would hope as this beds in that other Promela/SPIN users out there will also get
> > more involved over time.
>
> Thank, it is appreciated.
>
I'm also interested in tracking this, and I might be able to go after
some resources on the US side. I'll be in touch on that later, but if
any US users are tracking this too, or you know any with interest, I'd
love to talk about it.

> > It is expected that Promela models will be as static as the corresponding APIs.
> > They capture the specified behaviour of API calls, not their detailed
> > implementation.
> >
> > The python scripts should also be fairly stable, although I can see some
> > tweaking for a while to improve workflow issues that might arise.
> >
> > There are some extra python libraries that are required over and above what is
> > currently specified in rtems-central/requirements.txt
>
> This all makes sense to me. Thank you for taking the time to respond.
>
> Chris
> _______________________________________________
> devel mailing list
> devel at rtems.org
> http://lists.rtems.org/mailman/listinfo/devel