Repeated Requirements

[abakst]

Hi all,

I'm wondering if anyone has any ideas for how to effectively tackle the following problem. I have a system with several instances of a single type of subcomponent. If a single instance has, say, N requirements, then that means if I have C copies, I need to produce N*C requirements (almost identical, but changing some identifiers here and there, like X1, ...,XN.

(You can imagine a system with N identical sensor units that all feed in to a single 'logic' subcomponent that makes some kind of decision based on these sensor values -- in this case you really need to talk about each sensor unit)

I'm wondering if anyone can suggest a way that I might avoid so much repetition in providing the requirements, especially given that if changes are discovered later, they will have to be propagated to each near-duplicate requirement.

As an example, one idea is to simplify give requirements for each type of component only (in the example above, just give the Nrequirements for a sensor unit, plus for a logic subcomponent with C inputs) . I think this would work, but then checking realizability wouldn't be checking the realizability of the composition of the C sensors and so on.

I think the problem wouldn't be so much of an issue if there were an easy way to use a standard text editor to produce the requirements. I think the CSV format is close to this, but it seems importing the frettish sentences wraps them in quotes (e.g. as "FSM shall always Foo"), which means they don't get semantics generated for them.

Thanks!

[anmavrid]

Hi Alexander,

what you describe fits perfectly with the idea of FRET templates: you could create a template for a type of requirements and then have placeholders for identifiers (X1, ...,XN) that are changing in each requirement instance.

Here is information on how to use templates in FRET: https://github.com/NASA-SW-VnV/fret/blob/master/fret-electron/docs/_media/user-interface/writingReqs.md#templates-tab

and here is information on how to create a FRET template: https://github.com/NASA-SW-VnV/fret/blob/master/fret-electron/docs/_media/creatingTemplates/createTemplate.md

I would be happy to discuss FRET templates or other ideas further with you.

Thanks,
Anastasia

[abakst]

Thanks for the pointer to templates! I think these are close to what I'm looking for, but I do have some additional thoughts. I'm not sure how generally useful these would be, but I thought I'd share them here anyway. Let's consider the following set of requirements:

FSM shall always satisfy if S_0 > X_0 then Y_0
FSM shall always satisfy if S_1 > X_1 then Y_1
FSM shall always satisfy if S_2 > X_2 then Y_2
(etc.)

If possible, it would be nice to capture the extra structure that's there (i.e., the index is repeated across the variables S, X, and Y in each requirement). An immediate idea is that it might be handy to allow a template form (a lot like a macro) that would allow the moral equivalent of:

T(i) := FSM shall always satisfy if S_i > X_i then Y_i

In a slightly different but related scenario, now imagine I have maybe a half dozen such requirements, i.e.

FSM shall always satisfy if S_i > X_i then Y_i
FSM shall always satisfy !Y_i | !Z_i
FSM shall always  ... f(X_i, Y_i, Z_i, S_i)

(for a few valuations of i)

Another idea might be to parameterize a set of requirements by some identifiers, so maybe something like:

Template(S,X,Y) := FSM shall always satisfy S > X then Y
Template2(Y,Z) := FSM shall always satisfy !Y | !Z
F(S_i, X_i, Y_i, Z_i) := { Template(S_i, X_i, Y_i), Template2(Y_i, Z_i) }

and then allow instantiating this family in some parent requirement, i.e.

F(S_0, X_0, Y_0, Z_0), F(S_1, X_1, Y_1, Z_1) and so on.

[anmavrid]

I see what you are saying. Another way of describing such constraints in a concise way is through a quantified (first-order) logic formula. For example: "FSM shall always satisfy forall i 0<=i<N and (if s[i] > x[i] then y[i])", where N is known. Right?

[abakst]

Yes, exactly!