On 4/9/20 7:35 pm, Andrew Butterfield wrote: > Dear Chris, > > thanks for your feedback - much appreciated! > > Responses to your queries inline below. > >> On 3 Sep 2020, at 00:38, Chris Johns <chr...@rtems.org >> <mailto:chr...@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 <http://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.
Great. >> 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. Sounds good. I am looking forward to seeing the results. >> 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. Just so I understand, if the model and the API do not match the test will report a failure? >> 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 <http://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. That is fine. We understand few people often see the real hardware with flight software development. We are relaxed on how an architecture can reach tier-1, we need only one device from a family to run the tests with the results being published. My desire is to automatically monitor the test results and age out older results. > 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? The test output needs to be posted using the public rtems-tools.git `rtems-test` command. For public test results to be meaningful the tools used to generate the results need to be public. > My understanding is that as our project rolls out we will be running hardware > tests. This is understandable and what I would expect. The role of tiers in RTEMS is to bring the results out into the public so all users can view where each architecture and device family sits. I personally see value for hardware vendors having devices in tier-1 and I see value for large organisation like ESA expecting to see their selected hardware in tier-1. You and I will not make this happen. > 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. If the tests end up in the testsuite the tests will be required to pass on all supported architectures. We consider the range of architecture we support a real feature because the code needs to be clean. Chris _______________________________________________ users mailing list users@rtems.org http://lists.rtems.org/mailman/listinfo/users
