<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Dear Chris,<div class=""><br class=""></div><div class=""> thanks for your feedback - much appreciated!</div><div class=""><br class=""></div><div class="">Responses to your queries inline below.<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On 3 Sep 2020, at 00:38, Chris Johns <<a href="mailto:chrisj@rtems.org" class="">chrisj@rtems.org</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="">On 1/9/20 2:30 am, Andrew Butterfield wrote:<br class=""><blockquote type="cite" class="">Dear all,<br class=""><br class=""> I am involved the in the ESA sponsored project RTEMS-SMP, to add <br class="">tools and data for software qualification. Our focus is on the use <br class="">of formal techniques to assist in software verification.<br class=""></blockquote><br class="">Excellent :)<br class=""><br class=""><blockquote type="cite" class="">We have a developed a prototype for an approach that uses the SPIN<br class="">model-checker (<a href="http://spinroot.com" class="">spinroot.com</a>) to produce formal models of RTEMS API<br class="">behaviour, from which API tests can be generated. The formal models<br class="">form one way of specifying the desired behaviour for these APIs.<br class=""></blockquote><br class="">Spin looks nice. Its maturity and wide host support looks great.<br class=""><br class=""><blockquote type="cite" class="">We have developed a prototype demonstrator of this technique and are<br class="">now seeking feedback from the community. It is expected that a<br class="">suitably revised and updated version of this would become part of the<br class="">proposed RTEMS qualification tool-chain.<br class=""><br class="">The demonstrator can be found at:<br class=""> <a href="https://github.com/andrewbutterfield/manual-spin2tests" class="">https://github.com/andrewbutterfield/manual-spin2tests</a><br class=""></blockquote><br class="">The repo looks great. The approach looks suitable for our project.<br class=""><br class=""><blockquote type="cite" class="">Feedback on all aspects of this from a range of different perspectives<br class="">would be very welcome. <br class=""></blockquote><br class="">Will the results of your efforts be merged into the rtems-central repo?<br class=""></div></div></blockquote><div><br class=""></div>Yes - I believe so.<br class=""><blockquote type="cite" class=""><div class=""><div class=""><br class="">Is there any relationship between the spec files Sebastian is creating for the<br class="">APIs and your work? If not how would they be kept in sync or at a minimum how<br class="">would we know they do not match?<br class=""></div></div></blockquote><div><br class=""></div>The plan is for our work to be fully integrated with what Sebastian is building.</div><div>Our spin2test tool would be part of the qualification tools, and the tests we produce</div><div>would be integrated with the handwritten test suites. The test results would feed into</div><div>the tests analysis tools (coverage, etc..) and that analysis would end up as part of</div><div>the qualification datapackage.<br class=""><blockquote type="cite" class=""><div class=""><div class=""><br class="">How is the log from the test output used to validate the model?<br class=""></div></div></blockquote><div><br class=""></div></div><div>The test output shows what the test did, so it can be used by someone familiar with the</div><div>requirements to judge if the test expectations of correct behaviour are themselves correct.</div><div>So, yes, they can help in that regard.</div><div><br class=""></div><div><blockquote type="cite" class=""><div class=""><div class=""><br class="">I would like to see this work performed on a tier-1 architecture [1]. At this<br class="">point in time SPARC (and LEON) is not tier-1 because there are no test results<br class="">from hardware posted to build @ <a href="http://rtems.org" class="">rtems.org</a>. This leaves the ESA pre-qual project<br class="">with some choices. You could select a suitable target like a beagleboneblack and</div></div></blockquote><blockquote type="cite" class=""><div class=""><div class="">post hardware test results or encourage other members of the pre-qual project to<br class="">run the testsuite on a LEON and post the results. We could then move SPARC and<br class="">LEON to tier-1, something I personally would love to see.<br class=""></div></div></blockquote><div><br class=""></div>In one sense the ESA project has no choice - we have to work with leon3/gr712rc/gr740.</div><div>I should point out that a test generated by us has been run (standalone) on gr740 hardware at ESTEC.</div><div>Would it help if the results of that was posted? </div><div><br class=""></div><div>My understanding is that as our project rolls out we will be running hardware tests.</div><div><br class=""></div><div>However, the way I built the test executables was using waf configured for the above three BSPs,</div><div>and so it should be possible to do it for another tier-1 architecture.</div><div><br class=""></div><div>Thanks, Andrew<br class=""><blockquote type="cite" class=""><div class=""><div class=""><br class="">Thanks<br class="">Chris<br class=""><br class="">[1]<br class=""> <a href="https://docs.rtems.org/branches/master/user/hardware/tiers.html" class="">https://docs.rtems.org/branches/master/user/hardware/tiers.html</a><br class=""> <a href="https://git.rtems.org/rtems-tools/tree/config/rtems-bsps-tiers.ini" class="">https://git.rtems.org/rtems-tools/tree/config/rtems-bsps-tiers.ini</a><br class=""></div></div></blockquote></div><br class=""><div class="">
<div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">--------------------------------------------------------------------<br class="">Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204<br class="">Lero@TCD, Head of Software Foundations & Verification Research Group<br class="">School of Computer Science and Statistics,<br class="">Room G.39, O'Reilly Institute, Trinity College, University of Dublin<br class=""> <a href="http://www.scss.tcd.ie/Andrew.Butterfield/" class="">http://www.scss.tcd.ie/Andrew.Butterfield/</a><br class="">--------------------------------------------------------------------</div>
</div>
<br class=""></div></body></html>