Re: Integrating the Formal Methods part of Qualification

Dear Andrew, > It's great to see a move toward formal verification for RTEMS. Great to hear about other work in this space as well ! > 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

Re: Integrating the Formal Methods part of Qualification

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

Re: Integrating the Formal Methods part of Qualification

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

Re: Integrating the Formal Methods part of Qualification

On 6 Jul 2022, at 20:07, Gedare Bloom wrote: On Sun, Jul 3, 2022 at 7:49 PM Chris Johns wrote: On 2/7/2022 12:59 am, Andrew Butterfield wrote: On 1 Jul 2022, at 00:59, Chris Johns mailto:chr...@rtems.org>> wrote: On 28/6/2022 11:09 pm, andrew.butterfi...@scss.tcd.ie

Re: Integrating the Formal Methods part of Qualification

On Sun, Jul 3, 2022 at 7:49 PM Chris Johns wrote: > > On 2/7/2022 12:59 am, Andrew Butterfield wrote: > > On 1 Jul 2022, at 00:59, Chris Johns > > wrote: > >> > >> On 28/6/2022 11:09 pm, andrew.butterfi...@scss.tcd.ie > >> wrote: >

Re: Integrating the Formal Methods part of Qualification

On 2/7/2022 12:59 am, Andrew Butterfield wrote: > On 1 Jul 2022, at 00:59, Chris Johns > wrote: >> >> On 28/6/2022 11:09 pm, andrew.butterfi...@scss.tcd.ie >> wrote: >>> Dear RTEMS Developers, >>> >>> While the validation tests from

Re: Integrating the Formal Methods part of Qualification

-Original Message- From: Chris Johns On 28/6/2022 11:09 pm, 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

Re: Integrating the Formal Methods part of Qualification

On 1 Jul 2022, at 00:59, Chris Johns mailto:chr...@rtems.org>> wrote: On 28/6/2022 11:09 pm, 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

Re: Integrating the Formal Methods part of Qualification

On 28/6/2022 11:09 pm, 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. > >

Integrating the Formal Methods part of Qualification

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)