Verification Problem?

[nasa-sw-vnv]

Verification Problem?

[anmavrid]

Hello @SoftPro,

Let me see if I understand this correctly. So you have variables in the FRETish requirements that do not correspond to model variables. Why are these variables used in the requirements? Are they auxiliary expressions of model variables?

[SoftPro]

Hello, @anmavrid
I think my previous expression may not be very clear. You can take a look at this example.
Define the sub mode interval under a mode, and then define the specification based on the sub mode interval, but in fact, the sub mode is not defined in the system.

 in mode A the sys shall until conditionA satisfy modeB.
 in modeB unless P the sys shall after 1seconds satisfy P.
 in modeB when P the sys shall after 1 seconds satisfy !P.

But modelB does not exist in the model.

[anmavrid]

Hello @SoftPro,

Thanks for the example. I see that you define modeB as a submode of A.

Do I understand correctly that modeB should be true from the beginning of mode A until conditionA becomes true? So, essentially this is what "sets" modeB in requirement 1, so that modeB can be used in the other 2 requirements although it does not exist in the model.

[SoftPro]

Hello, @anmavrid
Yes, then if these requirements are verified using cocosim on simulink, is it impossible to verify these properties because the modeB variable does not exist in the model.

[anmavrid]

Got it! You can assign the modeB variable through the variable mapping in FRET (in the analysis portal). Let me work on your example and show you how to do that. I will get back to you.

[anmavrid]

Hi @SoftPro,

This is an excellent question. There are a couple of ways you can do that depending on whether you want to perform realizability analysis in FRET or verification of a Simulink model with CoCoSim. What would you like to do?

1. For realizability analysis:
   You can declare requirement 1 (in mode A the sys shall until conditionA satisfy modeB) as an assumption. You can do that by including the word assumption in the requirement ID (FRET requirement editor). In this case modeB can be assigned as controlled (output) variable in the FRET analysis portal.

2. For analysis with CoCoSim and for realizability analysis (but this solution might be more challenging:
   You can assign modeB as an internal variable (through the FRET analysis portal) and then provide the definition of the variable through "variable assignment" in the analysis portal. The definition of the variable would be something similar to the first requirement:
   modeB = in mode A and until conditionA
   Note that this is a temporal expression and thus, it might be challenging to express.

Please let us know if you have questions. Our team is here to support you! @andreaskatis @tpressburger

Thank you,
Anastasia

[SoftPro]

Hello, @anmavrid
Thank you very much for your answer. What I want is the second solution. The problem can be solved through intermediate variables.
Recently, I was studying how to convert fresh language into cocospec, but I found few papers. I don't know whether I can provide some more detailed information.I sent you an email a few days ago. If you can provide relevant information, I will be very grateful. If not, it's all right.

[anmavrid]

Absolutely - I am sending you more info.

Sorry, I missed your email because it was sent to my private gmail. For quicker communication please email us at: [email protected], [email protected], and [email protected].

[anmavrid]

I am closing this issue because the discussion has transferred.