Add traceability tooling proposal

[thanethomson]

This draft PR focuses on implementation considerations to do with #11, and so far contains some of the background research I've managed to gather today in terms of the (rather broad) field of requirements management and the current state-of-the-art in terms of requirements management tooling. NB: There could be much more out there.

The Domain Analysis background section is in particular need of attention, I think.

At the moment, I think the next steps I'll take for working on this doc will be:

• [x] Define all users/stakeholders we intend to involve in the specification/validation process
• [x] Define what each of those users want out of the tooling
• [x] Clarify whether existing tools can be used or where they are deficient
• [x] Outline what an MVP would look like that could implement #11 (including formats and practical examples of how to write a spec, code and tests)

Traceability: Rendered Tooling: Rendered

[thanethomson]

Have there been any efforts at open source tools for requirements management? Did you get any hits searching specifically for relation between requirements tracing and TLA+?

The only open source tool I can find right now is Eclipse Capra. Its UI seems really complex, like most of the other tools for requirements management.

Haven't managed to find any links between traceability and TLA+ yet unfortunately.

[konnov]

I also had the impression that the commercial tools are overengineered. I don't think that TLA+ has been applied in any industry that requires certification. We should probably look at traceability and Event-B, which is a general formal language that was applied to safety-critical systems.

[thanethomson]

I've added some more detail to the stakeholders and their needs that I can identify at this point, along with what I can deduce in terms of:

1. The domain model for general requirements management software.
2. Our domain model for requirements management for our VDD process.

The implementation recommendations are still very much incomplete at this point.

I also had the impression that the commercial tools are overengineered. I don't think that TLA+ has been applied in any industry that requires certification. We should probably look at traceability and Event-B, which is a general formal language that was applied to safety-critical systems.

I've started looking at Event-B, but it seems as though you need to buy this textbook to get a good grasp of what Event-B's all about?

[thanethomson]

Thanks a lot for the very comprehensive document! I also learned a lot. The big question for me is how we balance the need to trace requirements, defects, etc. with the manual effort to add tag annotations. From my short experience with writing English specs, just tagging is easy, but referencing tags from other documents, etc. can be involved and time-consuming. If this could be done in an interactive mode that would be great. I guess when writing code that would be similar. I guess the workflow would be that one works on an implementation, and then at some point one adds annotations, perhaps as part of CI?

Cool! My current sense is that, since the relationships between specs, models, implementation code and test code are complex ones conceptually (and probably practically impossible in most cases for a computer program to automatically infer), we will have to manually put these tags into, e.g., comments in models and code as we code them.

Where CI-based tooling (which could also be run locally on one's own machine) will help out is in automatically detecting things like:

1. Are references in models/code out of date compared to the spec?
2. Are there dangling references?
3. Is there unimplemented code?
4. How do defects (i.e. issues captured on GitHub) relate to the specification and models/code?

We then need to decide on how to relay this information to all stakeholders. My current sense is that we should automatically produce some kind of documentation (e.g. a static web site) that has embedded links between all of our artifacts for easy navigation.

The challenge with building an IDE plugin to help with navigation is that people might use different IDEs for (1) writing specs, (2) writing models, and (3) writing Rust code. We'll need to think about whether IDE plugins would be useful here, and, if so, which IDEs to support.

[shonfeder]

The challenge with building an IDE plugin to help with navigation is that people might use different IDEs for (1) writing specs, (2) writing models, and (3) writing Rust code. We'll need to think about whether IDE plugins would be useful here, and, if so, which IDEs to support.

I suggest we use the Language Sever Protocol, which has support in virtually every reasonable IDE/editor. IIUC, can make a CLI-based executable that serves up the needed analysis from a corpus via the protocol, and use that as the backend for all editors. Then it should be a relatively small lift to add in support for any particular IDE and, more importantly, we may also be able to leverage the LSP program in other contexts (like for CI and web apps).

[thanethomson]

I suggest we use the Language Sever Protocol, which has support in virtually every reasonable IDE/editor. IIUC, can make a CLI-based executable that serves up the needed analysis from a corpus via the protocol, and use that as the backend for all editors. Then it should be a relatively small lift to add in support for any particular IDE and, more importantly, we may also be able to leverage the LSP program in other contexts (like for CI and web apps).

I was thinking about the option of implementing a LSP, but there's additional complexity here because we'd effectively have to build an embedded language server protocol. We may effectively need to "proxy" the LSPs for Markdown, TLA+ and Rust.

I've personally never built anything like that before, so, if we go ahead with this project (which I think we should), and if we decide to try the LSP route, we should definitely do some kind of PoC during one of the next deep flow weeks to de-risk it.

[shonfeder]

I agree we should be careful to do de-risking. My main concern is to push against this dilemma:

We'll need to think about whether IDE plugins would be useful here, and, if so, which IDEs to support.

As much as possible, I think we should focus on a generally useful backend that can be leveraged by any IDE, and then build in lightweight support for particular IDEs as needed, rather than guiding implementation by focusing on support for particular products.

[thanethomson]

As much as possible, I think we should focus on a generally useful backend that can be leveraged by any IDE, and then build in lightweight support for particular IDEs as needed, rather than guiding implementation by focusing on support for particular products.

I'd just caution against thinking that the per-IDE integration of a language server would be lightweight, especially given the unknowns in the embedded LSP. That's part of what I think we'd need to prove with a PoC.

[shonfeder]

I'd just caution against thinking that the per-IDE integration of a language server would be lightweight,

I can't speak to the difficulty of an embedded LSP, and maybe that's not the right approach due to overhead. But what about simple auto-complete plugins triggered by a single command? If we have a backend able to parse out the files where we store the references dictionary, then it should be easy to add plugins that just call that, no? At least in Vim and Emacs, I think such functionality should be fairly easy to add given the right backend, and I'd hope it wasn't heaps more difficult on other editors.

[thanethomson]

I can't speak to the difficulty of an embedded LSP, and maybe that's not the right approach due to overhead. But what about simple auto-complete plugins triggered by a single command? If we have a backend able to parse out the files where we store the references dictionary, then it should be easy to add plugins that just call that, no? At least in Vim and Emacs, I think such functionality should be fairly easy to add given the right backend, and I'd hope it wasn't heaps more difficult on other editors.

Not sure about that either 😁 I think the only way we'll know for sure is if we actually build the PoC.

[konnov]

I've started looking at Event-B, but it seems as though you need to buy this textbook to get a good grasp of what Event-B's all about?

Well, that is part of the problem with the tools for critical systems. There are a few academic papers that talk about Event-B. I have never read a real book on it.

[konnov]

We then need to decide on how to relay this information to all stakeholders. My current sense is that we should automatically produce some kind of documentation (e.g. a static web site) that has embedded links between all of our artifacts for easy navigation.

I support that. Otherwise, we might very easily end up with an overengineered tool :-)

[thanethomson]

I've expanded the recommended architecture and have added a few more aspects that I'd previously forgotten. For example, we'd eventually need the compiler to also pull in information from GitHub/GitLab to extract information on defects. It's obviously not critical for an MVP, but would be necessary in a comprehensive tool in future.

[thanethomson]

Oh, the other thing we need to consider in the VDD process in general, is: do we need to explicitly distinguish between requirements and acceptance criteria? I know in some fields they do.

[thanethomson]

Cool, so I've updated both the tooling proposal as well as the original traceability spec according to the conversation here.

It now exclusively uses PHP Markdown Extra's Definition Lists format for defining tags. The current traceability spec doesn't include any of the shortcuts I've mentioned previously.

As you can see here, it doesn't render too badly on GitHub. I'm sure we can make it look much nicer though once we pass it through our own tooling.

[konnov]

It looks nice. So we got rid of |...| in the tag definitions? That will probably work, due to the unique syntax of tags. One thing I am worried about with this lazy syntax is that it would be hard for the user to figure out a fully qualified tag name. The user will have to go up the hierarchy to assemble the full tag.

[thanethomson]

It looks nice. So we got rid of |...| in the tag definitions? That will probably work, due to the unique syntax of tags. One thing I am worried about with this lazy syntax is that it would be hard for the user to figure out a fully qualified tag name. The user will have to go up the hierarchy to assemble the full tag.

Yes, since Markdown definition lists provide the kind of structural elements we're looking for (i.e. associating a specific string with a specific chunk of text) there's no need for such tag definition syntax.

With regard to the lazy syntax, that's just a suggestion for convenience. Users who would be confused by the lazy syntax are more than welcome to use the fully qualified tag syntax. My current thinking is that you'd also be able to mix the two types of syntaxes if you really wanted. Also, our tooling would automatically expand the lazy syntax into the full syntax.

One thing I wanted to ask: do you need to define tags in models? Or is the only place where you'll define tags in specifications?

[konnov]

I believe that tags will be used in the English specs and TLA+ specs, but not in the MC*.tla modules, which are used to check TLA+ specs for the specific parameters.

[shonfeder]

I have a thought re:

Yes, since Markdown definition lists provide the kind of structural elements we're looking for (i.e. associating a specific string with a specific chunk of text) there's no need for such tag definition syntax.

I think we have two different concerns here:

1. How do we that a tag is a definiendum. This is a question of identifying lexemes. In terms of HTML, it only concerns span elements.
2. How do we express that some block of text is a definiens. This is a question of syntactic structure. In terms of HTML, it is about determine the scop of a block-level groupings.

If we are saying: the only time any tag definition will occur is when using definition lists, and definition lists will only be used to define requirement tags, then we are probably OK with not having an identifier that indicates tags lexically. However, if we are going to be introducing tag definitions not in markdown (e.g., in TLA+ comments?), or putting them also in heading elements, or if we want to be able to potentially use definition lists for other things, then, IMO, we should probably still stick to having a clear identifier of when tags are a definiendum. Personally, I'm inclined towards the latter, but I'm the not going the be the primary user.

[thanethomson]

Makes sense @shonfeder 👍 Also, from our meeting earlier today, given that we may want to define tags in TLA+ specifications (most likely in comments), and those tag definitions will need to be clearly distinguishable from ordinary comments, we will probably want a consistent syntax used across both TLA+ and human language specifications.

So should we go back to tag definitions being enclosed by pipe symbols, like |TRC-TAG.1|? References will still, in Markdown, TLA+ and Rust code, be made using square brackets like [TRC-TAG.1].

An expanded example:

...

## 3. Traceability properties

We need a solution that satisfies the following properties:

|TRC-TAG.1|
: Tagging a logical unit should be easy.

|TRC-REF.1|
: Referencing a logical unit should be easy.

...

[shonfeder]

That looks pretty readable to me. An added benefit is that, if we want to allow tag defs in any other elements (e.g., in list elements or headings), we'll be able to easily identify them with one consistent set of notation, and this will work to identify them in any other markup language we made need to add them into.