Using model checking to do test generation for RTEMS

[Andrew Butterfield]

Dear Chris,

 thanks for your feedback - much appreciated!

Responses to your queries inline below.

> On 3 Sep 2020, at 00:38, Chris Johns <chrisj at rtems.org> wrote:
> 
> 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?

Yes - I believe so.
> 
> 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?

The plan is for our work to be fully integrated with what Sebastian is building.
Our spin2test tool would be part of the qualification tools, and the tests we produce
would be integrated with the handwritten test suites. The test results would feed  into
the tests analysis tools (coverage, etc..) and that analysis would end up as part of
the qualification datapackage.
> 
> How is the log from the test output used to validate the model?

The test output shows what the test did, so it can be used by someone familiar with the
requirements to judge if the test expectations of correct behaviour are themselves correct.
So, yes, they can help in that regard.

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

In one sense the ESA project has no choice - we have to work with leon3/gr712rc/gr740.
I should point out that a test generated by us has been run (standalone) on gr740 hardware at ESTEC.
Would it help if the results of that was posted? 

My understanding is that as our project rolls out we will be running hardware tests.

However, the way I built the test executables was using waf configured for the above three BSPs,
and so it should be possible to do it for another tier-1 architecture.

Thanks, Andrew
> 
> 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

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.rtems.org/pipermail/users/attachments/20200904/f96f9f49/attachment.html>