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. 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 Feedback on all aspects of this from a range of different perspectives would be very welcome. Regards and Thanks, Andrew Butterfield -------------------------------------------------------------------- Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@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/ -------------------------------------------------------------------- _______________________________________________ users mailing list users@rtems.org http://lists.rtems.org/mailman/listinfo/users