Confusing conflits on Realizability checking

[anaisac]

Hello everyone :)

I'm going to post this here, since is not an issue with the tool itself, just me trying to figure out more :)

I've changed a bit my requirement to have a more explicit attribution. And when I did the realizibility checking, I got a conflict that I was not expecting to have, let me show you the printscreen:

"R6" is the requirement name so I see that it shows up to give the "final" answer if the requirement is realizable or not.
"TLS_Keys" is my component so I expect it does not have any weight on the checking.
"valid" is the attribution value that I want to give, and this one I expect to be true or false.
"entity" I was expecting it to be just the receiver of the attribution, so that's why I put it as input in the variable mapping.
I'm not understanding why the "entity" has a start value of false, I was expecting that it always received the value that I was giving to it, and that the "entity" was neutral?! .
Am I confusing concepts here? Can you help me understand what I'm doing wrong?

This is my variable mapping.

If necessary I can provide the analysis files :)

[andreaskatis]

Hi @anaisac,

I think there is some confusion regarding the different variable types and their use. Roughly speaking, considering a system component (TLS_keys), you currently have the following:

• entity is an Input to TLS_keys: In other words, TLS_keys monitors the values of entity, but has no control over what those values should be. That is, the system's input values cannot be modified (except for a category of requirements flagged as "assumptions", which I will mention further below).
• valid is an Internal varible of TLS_keys: Variables of type Internal can serve as macros to more complex expressions that involve Input, Output and other Internal variables. Internals can be typically understood as variables whose values are computed by the system for further use. In other words, they are controllable by the system, but we have already defined what exactly they compute.

One crucial information missing at this point is the Lustre assignment that you've given to valid. Considering the counterexample, I assume that you've set this to true. This means that valid is essentially a constant with value true, and that's what the system will always set it to.

Given this, the requirement that you checked is unrealizable. The reason is that the requirement in its current form expresses an expectation that entity = valid holds for every value of entity. Consequently, this is not possible since entity can be set to false while valid has been defined to remain constantly true. Therefore, the requirement is declared as unrealizable.

Given that the above makes sense, what you can further do is create requirements that specifically introduce constraints over inputs. We refer to such requirements as "assumptions". A requirement is an assumption if it contains the string "assumption" in its Requirement ID (e.g. "R6_assumption"). Assumptions will be handled differently during analysis than regular requirements. In your case here, one way to resolve unrealizability (again, assuming that valid is assigned to true) would be to introduce an assumption like the one below:

TLS_keys shall always satisfy entity.

This assumption simply states that for the input entity we assume that its value is always true. While this is a very trivial example (and probably not useful), I hope it helps you understand how assumptions are used to introduce constraints over Input variables.

Sidenote: assumptions that involve Internal and Output should refer to such values using our pre predicates (see our Previous for more details). Intuitively, system inputs can only depend on previous values of internals and outputs.

Hopefully this helps. Please let us know if you have further questions.

Andreas

[anaisac]

Hi Andreas :)

Definitively I was confusing the use cases of each type of variables. Thank you so much for the detail explanation.
At this point I think I'm going to stick with requirements use constraints instead of inputs.
However that one with assumption might be interesting but I don't know if I will explore it now.

The example was perfect, exactly what I was looking for at this moment, and the values you assumed were the correct ones, so I will change on my side. Thank you :)

Actually, I will keep this thread open for my next questions because I'm assuming is still from my lack of full understanding with the variables attribution.
In another requirement I created this:

And I was expecting that the time simulation was capable of giving me some kind of threshold (maybe is not possible, or I'm doing wrong). The idea was that if the "ECU_ROM_size" inferior to 70, the time simulation show it as true, and failed with as soon the ECU_ROM_size was above 70. And I would like to have this kind of "play" in the time simulation. But I think I'm not using the correct attribution on the Variable mapping to allow me to play around with the threshold values. Or do I need to have the 2 requirements for intersect them?

[andreaskatis]

Hi @anaisac ,

The requirement in this example expresses that ECU_ROM_Size <= 70 in every timepoint of the system's execution. Since ECU_ROM_Size is a constant with value 100, the counterexample is a single timepoint. This makes sense, because the requirement would be violated at the very beginning of the system's execution, so there's no point in "looking any further".

One trivial way to get what you describe would be to change the requirement's timing value from always to something weaker, relaxing the temporal constraint as a result. For example:

The sw_package_size shall within 3 ticks satisfy ECU_ROM_Size <= 70

Obviously, the semantics change drastically in this case. The diagrammatic semantics and the simulator in the requirements editor should help towards identifying what you ultimately intend to capture.

Another, perhaps more interesting way to get what you intend is to change the assignment of ECU_ROM_Size to something that will yield counterexample of length greater than 1. Try the following:

65 -> pre(ECU_ROM_Size) + 1

This Lustre expression sets the value of ECU_ROM_Size to 65 in the first timepoint, then decrements it by 1 in each subsequent timepoint. Since your requirement states that ECU_ROM_Size >= 70 must always hold, the counterexample will indicate that this is not the case because the value 71 is reachable in 7 steps.

Again, ultimately it all depends on what you intend to capture as part of the system's behavior. Hopefully these examples can help you a bit more.

Best,

Andreas

[anaisac]

Hello @andreaskatis,

The idea here would be more on: I received the "sw_package_size" and I check the size of it.
In case the sw_package_size<=70ECU_ROM_Size the requirement holds true in every trace. I case sw_package_size>70ECU_ROM_Size the requirement will be false in every trace.

Now that I'm seeing from your perspective, I think my requirement writing is not really translating the idea I want, but those examples definitively help me. I will think about it in another way.

The thing is, the set of requirements I'm using doesn't have much on changing in time, they are mostly ubiquitous(prescribe format), process commands and state transitions at first trace point. This one from ROM was the only one that I say is identifiable as being a check bound and I also have 3 set diagnostic flags that need to happen at first trace point.