Dear Andrew, It's great to see a move toward formal verification for RTEMS.
>From our side (TU Dortmund in Germany and the University of Twente in the Netherlands), we recently adopted Frama-C to verify ICPP and MrsP. A potential deadlock is successfully identified, and a remedy is provided. The result will be presented in EMSOFT this year ( https://ieeexplore.ieee.org/document/9852753/), and the verification framework is publicly released here: https://github.com/tu-dortmund-ls12-rt/Resource-Synchronization-Protocols-Verification-RTEMS Due to the double-blind review process, I cannot chime in earlier in this thread. Today earlier I have seen your patches regarding the chapter you proposed. I wonder if you could take our contribution into account when you organize the chapter? A preprint can be found here <https://www.researchgate.net/publication/362599165_Formal_Verification_of_Resource_Synchronization_Protocol_Implementations_A_Case_Study_in_RTEMS>. (The corresponding ticket will be prepared, and the patch together with a test case will be submitted) Best, Kuan-Hsun On Fri, Jul 22, 2022 at 12:37 PM andrew.butterfi...@scss.tcd.ie < andrew.butterfi...@scss.tcd.ie> wrote: > Dear RTEMS developers, > > > > thanks for the feedback below - I want to wrap this up and move to the > next step. > > > > I propose to produce a complete draft of a formal methods section for the > Software Engineering manual in rtems-docs > > This will add a "Formal Verification" section just after the existing > "Test Framework" section. > > > > This will allow developers to get a much better idea of what is proposed, > and for me to get feedback. > > > > For now, the section will state clearly at the start that this is a > proposal and that the tooling and resources it describes > > won't yet be available in RTEMS proper. > > > > Files likely to be modified in rtems-docs: > > eng/index.rst > > common/refs.bib > > > > I'll add in eng/formal-verification.rst > > > > I'll then submit patches for review in the usual way. > > > > Regards, > > Andrew > > > > > > -------------------------------------------------------------------- > 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/ > -------------------------------------------------------------------- > > > > > > On 11/07/2022, 12:43, "devel on behalf of andrew.butterfi...@scss.tcd.ie" > <devel-boun...@rtems.org on behalf of andrew.butterfi...@scss.tcd.ie> > wrote: > > > > On 6 Jul 2022, at 20:07, Gedare Bloom <ged...@rtems.org> wrote: > > > > On Sun, Jul 3, 2022 at 7:49 PM Chris Johns <chr...@rtems.org> wrote: > > > On 2/7/2022 12:59 am, Andrew Butterfield wrote: > > On 1 Jul 2022, at 00:59, Chris Johns <chr...@rtems.org > <mailto:chr...@rtems.org>> wrote: > > > On 28/6/2022 11:09 pm, andrew.butterfi...@scss.tcd.ie > <mailto:andrew.butterfi...@scss.tcd.ie> wrote: > > Dear RTEMS Developers, > > While the validation tests from the RTEMS pre-qualification activity are > now merged into the RTEMS master, the work done in investigating and > deploying formal methods techniques is not yet merged. > > The activity had two main phases: a planning phase (Nov 2018-Oct 2019) > that explored various formal techniques, followed by an execution phase > (Oct 2019-Nov 2021) that then applied selected techniques to selected > parts of RTEMS. Some discussions occurred with the RTEMS community > via the mailings lists over this time. A short third phase (Nov 2021 - Dec > 2021) > then reported on the outcomes. Each phase resulted in a technical report. > > The key decision made was to use Promela/SPIN for test generation, and > to apply it to the Chains API, the Event Manager, and the SMP scheduler > thread queues. This involved developing models in the Promela language > and using the SPIN model-checker tool to both check their correctness > and to generate execution scenarios that could be used to generate tests. > Tools were developed using Python 3.8 to support this. Initial > documentation > about tools and how to use them was put into the 2nd phase report. > > > Congratulations for the work and results you and others have managed to > achieve. > It is exciting to see this happening with RTEMS and being made public. > > We now come to the part where we explore the best way to integrate this > into RTEMS. I am proposing to do this under the guidance of Sebastian > Huber. > > The first suggested step is adding in new documentation to the RTEMS > Software Engineering manual, as a new Formal Methods chapter. This would > provide some motivation, as well as a "howto". > > I assume that I would initially describe the proposed changes using the > patch > review process described in the section on Preparing and Sending Patches in > the User Manual. > > How do you feel I should best proceed? > > > It is hard for me to answer until I understand what is being submitted and > who > maintains it? I am sure you understand this due to the specialised nature > of the > work. > > > Indeed, I quite agree. I have some short answers below, with suggestions. > > > Thanks. > > +1 > > > > > What will be submitted, ie SPIN files, scripts, etc? > > > Promela/SPIN model files (ASCII text, C-like syntax) > C template files (.h,.c) to assist test code generation > YAML files to provide a mapping from model concepts to RTEMS C test code > python scripts to automate the test generation > Documentation - largely RTEMS compliant sphinx sources (.rst) > > > Where are you looking to add these pieces? > > > Everything except the documentation could live in a top-level folder > ('formal') > in rtems-central. > In fact there is no particular constraint from my perspective for where > they can go. > > > Using rtems-central is fine. > > Do they require anything currently located in rtems-central? Are the > models or YAML files related to the current specification files? I > know I'm guilty of not spending the time yet to deeply learn > rtems-central, but I would like to know that these files will fit > within that repo as it currently is intended to operate. > > > > At the moment there is nothing in rtems-central directly related to this. > All the python > > scripts there support the tools/specs that Sebastian and colleagues > developed. > > I can see a new top-level script being added here to support the formal > stuff. > > > > It is possible that we might introduce a new specification item that > integrates > > in with the spec system that is used to trigger the Spin test generations. > I'll discuss the > > best wat to do this with Sebastian. > > > > > > > RSB should be taught how to build the necessary host tools to run > Promela/SPIN. > > > > Spin is open source under a BSD 3-clause license, available from > spinroot.com, > > and also via https://github.com/nimble-code/Spin. It is written in C and > has very few > > dependencies. I'm not sure what is involved in adding it to the RSB, but I > guess > > Sebastian will know. > > > > The plan would be to add the pertinent parts of our project documentation > into > new chapters > in the RTEMS software engineering manual. So that would be eng/ in the > rtems-docs repo. > > > Great. > > +1 > > A new section in the eng should be suitable. I would actually > recommend using > https://docs.rtems.org/branches/master/eng/test-framework.html# as a > good example. > > > > Thanks - that very helpful. I think our section should immediately follow > that one. > > All we need now is a suitable title. "Formal Test Framework"? > > > > > > How is the verification run against the code? Do we manage regression > testing > and is that even possible? > > > The python scripts basically run SPIN in such a way as to generate > scenarios > that model > correct behaviour which then get turned into standard RTEMS test programs. > These all > get added into a new testsuite in the rtems repo (testsuites/models, say). > They are properly integrated into the RTEMS test system, so get built and > run by > waf. > This is similar to how the tests generated by Sebastian in > testsuites/validation > are handled. > > From the perspective of a user that works out of git.rtems.org/rtems > <http://git.rtems.org/rtems>, > there will be no obvious impact - just some extra tests in among the ones > that > already exist. > > > Thanks and this make sense. > > > > > I hope my simple questions highlight a lack of understand on how this > works and > how we maintain it and use it once integrated. > > > I intend to continue to work and maintain this for the foreseeable future. > I > would hope as this beds in that other Promela/SPIN users out there will > also get > more involved over time. > > > Thank, it is appreciated. > > I'm also interested in tracking this, and I might be able to go after > some resources on the US side. I'll be in touch on that later, but if > any US users are tracking this too, or you know any with interest, I'd > love to talk about it. > > > > Indeed - that would be good. > > > > Andrew > > > > It is expected that Promela models will be as static as the corresponding > APIs. > They capture the specified behaviour of API calls, not their detailed > implementation. > > The python scripts should also be fairly stable, although I can see some > tweaking for a while to improve workflow issues that might arise. > > There are some extra python libraries that are required over and above > what is > currently specified in rtems-central/requirements.txt > > > This all makes sense to me. Thank you for taking the time to respond. > > Chris > _______________________________________________ > devel mailing list > devel@rtems.org > http://lists.rtems.org/mailman/listinfo/devel > > > _______________________________________________ > devel mailing list > devel@rtems.org > http://lists.rtems.org/mailman/listinfo/devel > -- Diese Mail wurde mobil geschrieben. Etwaige Rechtschreibfehler sind volle Absicht und als großzügiges Geschenk zu verstehen.
_______________________________________________ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel