Using model checking to do test generation for RTEMS

[Andrew Butterfield]

Dear all,

 I am involved the in the ESA sponsored project RTEMS-SMP, to add 
tools and data for software qualification. Our focus is on the use 
of formal techniques to assist in software verification.

We have a developed a prototype for an approach that uses the SPIN
model-checker (spinroot.com) to produce formal models of RTEMS API
behaviour, from which API tests can be generated. The formal models
form one way of specifying the desired behaviour for these APIs.

We have developed a prototype demonstrator of this technique and are
now seeking feedback from the community. It is expected that a
suitably revised and updated version of this would become part of the
proposed RTEMS qualification tool-chain.

The demonstrator can be found at:
  https://github.com/andrewbutterfield/manual-spin2tests


Feedback on all aspects of this from a range of different perspectives
would be very welcome. 

Regards and Thanks,

  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/
--------------------------------------------------------------------