Using model checking to do test generation for RTEMS

[Chris Johns]

On 1/9/20 2:30 am, Andrew Butterfield wrote:
> 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.

Excellent :)

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

Spin looks nice. Its maturity and wide host support looks great.

> 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

The repo looks great. The approach looks suitable for our project.

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

Will the results of your efforts be merged into the rtems-central repo?

Is there any relationship between the spec files Sebastian is creating for the
APIs and your work? If not how would they be kept in sync or at a minimum how
would we know they do not match?

How is the log from the test output used to validate the model?

I would like to see this work performed on a tier-1 architecture [1]. At this
point in time SPARC (and LEON) is not tier-1 because there are no test results
from hardware posted to build @ rtems.org. This leaves the ESA pre-qual project
with some choices. You could select a suitable target like a beagleboneblack and
post hardware test results or encourage other members of the pre-qual project to
run the testsuite on a LEON and post the results. We could then move SPARC and
LEON to tier-1, something I personally would love to see.

Thanks
Chris

[1]
 https://docs.rtems.org/branches/master/user/hardware/tiers.html
 https://git.rtems.org/rtems-tools/tree/config/rtems-bsps-tiers.ini