Using model checking to do test generation for RTEMS
chrisj at rtems.org
Wed Sep 2 23:38:14 UTC 2020
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.
> 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:
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 . 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.
More information about the users