Integrating traceability concerns in VDD process

[milosevic]

Issue raised by @konnov, @josef-widder and @adizere.

• We have to figure out traceability. Designing the code will be an iterative process. How we keep the code and TLA+ in sync during change is a challenge I think.
• Perhaps we can introduce explicit versioning of code & spec artefacts. And enforce versioning as a part of the VDD process.
• We also need a common mechanism to refer to the individual parts of the properties (requirements), pre- and post-conditions, etc. These concepts have been formalized and standardised in the aircraft industry. However, it is hard to find an open and comprehensive description of the processes, as their certification processes have been commercialised. (Reading the standards themselves does not help much.) I just googled for a high-level overview. This document ( https://www.cadence.com/content/dam/cadence-www/global/en_US/documents/solutions/aerospace-and-defense/do-254-explained-wp.pdf) at least gives some ideas.

[adizere]

Had a look over "DO-254 explained" document [1]. We can consider two types of traceability it seems:

• iterative traceability: this is the problem of tracking changes to the same component, which can probably be solved with explicit versioning.
• traceability of refinement: this is the problem of tracking the refinement from a higher-level component into a lower-level component.

Note that by "component" I mean a "unit of review of verification". So examples of components are: a code block, or a TLA+ module, or an English spec defining a problem abstractly.

-- [1] https://www.cadence.com/content/dam/cadence-www/global/en_US/documents/solutions/aerospace-and-defense/do-254-explained-wp.pdf

[josef-widder]

Thanks for the pointer!

I guess the main problem is combination of the two types. E.g., if I have some temporal property A, and then in the process of refinement I figure out that A needs to be rewritten, I have to update to A2. Now it becomes complicated if other components use A. Should A still be there and A2 added, etc. In order even to understand the situation, it would be important to understand what components refer to A. For that the matrix of which Igor talks about would be important...

[konnov]

I think I have a clear idea in my head now. So I have started writing a proposal.

[konnov]

See the pull request #11