On Fri, Nov 25, 2022 at 12:45 AM Sebastian Huber <sebastian.hu...@embedded-brains.de> wrote: > > On 24/11/2022 14:41, andrew.butterfi...@scss.tcd.ie 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. >
My intuition here is that with suitable How-To's written and the code pushed, we don't need such detailed implementation notes. Just point the interested reader to the implementation, and to more general documentation/reports about Promela or even a tech report published by the group that did this work. > -- > embedded brains GmbH > Herr Sebastian HUBER > Dornierstr. 4 > 82178 Puchheim > Germany > email: sebastian.hu...@embedded-brains.de > phone: +49-89-18 94 741 - 16 > fax: +49-89-18 94 741 - 08 > > Registergericht: Amtsgericht München > Registernummer: HRB 157899 > Vertretungsberechtigte Geschäftsführer: Peter Rasmussen, Thomas Dörfler > Unsere Datenschutzerklärung finden Sie hier: > https://embedded-brains.de/datenschutzerklaerung/ _______________________________________________ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel