> On 25/11/2022 07:46, Sebastian Huber <sebastian.hu...@embedded-brains.de>
> wrote:
>> On 24/11/2022 14:41, andrew.butterfi...@scss.tcd.ie wrote:
>>> On 16/11/2022 16:44, Gedare Bloom <ged...@rtems.org> wrote:
>>> Section 9.7 "RTEMS Formal Model Guide" seems like it includes both
>>> some aspects of a How-To but also a lot of details that might be
>>> better as a separate document specific to the Promela/Verification
>>> detailed implementation. The point of the RTEMS Software Engineering
>>> manual is to provide developers with the guidelines of how to work
>>> with RTEMS. This section is very detailed about the implementation of
>>> specific models and feels unbalanced with the rest of the new section.
>>> For example, this section is about 3/5 of the entire "Formal
>>> Verification" section.
>>
>> I agree - this was what struck me after I had sent the patch set. In a
>> sense I think we need a new top-level document, analagous to the Classic
>> API and POSIX API guides.
>
> I am not sure if a new top-level document is really the best option.
> From my point of view, the RTEMS Software Engineering manual should
> cover everything useful for the general RTEMS maintainer. The models
> cover core services of RTEMS. With different documents you just have to
> open more documents and cross referencing will be more difficult. I am
> more in favour of a top-level chapter in the manual or some sort of an
> appendix chapter.
Now that the integration of the formal models and tools is in progress, I want
to revisit this issue. Yes, the models cover core services, but those are
described in other documents like the Classic API guide (and POSIX). It would
seem that a better place to put any model documentation would be in those
guides.
However, the formal verification/qualification is something very new, and I’m
not sure how regular users would feel about that kind of extra material, at
least at this early stage of adopting qual/FV techniques.
For now, I am going fixup all the other issues raised by Gedare,
and submit a v2 patch set.
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/
--------------------------------------------------------------------
_______________________________________________
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel
