informalsystems / informalsystems/vdd

Integrating traceability concerns in VDD process

Open
#4 4 comments 0 reactions 0 assignees View on GitHub
Dominant language
No language data
Stars
21
Forks
0
PR merge metrics
No merged PRs in 30d

Description

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.

Contributor guide

No contributing guide indexed for this repository

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.