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 _______________________________________________ users mailing list users@rtems.org http://lists.rtems.org/mailman/listinfo/users
