A/G Contract Sample Time Handling

[StefanoCentomo]

Hi,

How can I manage time granularity in Cocosim Contract requirements block?

For instance, let consider these three simple requirements in FRET:

Component shall always satisfy in_1 > 0.0
Component shall always satisfy in_2 > 0.0
if out < 5.0 Component shall within 5 seconds satisfy out > 5.0

I have imported those requirements into CoCosim and I have noticed that the the generated contract block does not have any timing settings in its properties (the usual sample rate for simulink block).

Here you can find two Simulink examples with different settings.
Example.tar.gz

Both examples are composed by a simple model that only perform a sum between in_1 and in_2.
The output is propagated into "out" port.

The contract block is the one generated by the initial requirements.

The model is stimulated by a constant of 1, that validate the first two requirements (in_1>0.0 & in_2 > 0.0), but not the third (out < 5.0 with timing constraint).

In System_with_contracts.slx model, if you launch a simulation of 10 seconds you will notice that the contract block return false after only one second.
We should expect that the contract returns True for the first 5 seconds, and then return always false (due to the third requirement).

From my point of view, the main issue comes from the fact that the contract block does not have internal knowledge of the simulation.
Each simulation step of the contract represent a timing advance of 1 second.
The default variable-step solver of simulink executes all the involved blocks (included the contract one), with a variable simulation step that is not 1 second (as the contract block internally seems assume).

In System_with_contracts_v2.slx model, I have changed the sample rate of input and output port of the Contract block, setting it to 1, instead of -1 (meaning that is simulink to provide a sample rate).

I have tried also changing the global solver using a fixed-step one, forcing the fixed step to 1 second.
In this case, the contract block works correctly.

I have tried also changing the step to 2 seconds and the contract block changed its output to false at time 10 (after exactly 5 executions of contract block).

I think this issue could be solved adding to the contract the knowledge of the global simulated time and also the simulation step (sample time in simulink).

Are you planning to improve Contract time handling in future versions of CoCoSim?
I think this aspect could affect also Fret framework, in particular CoCoSpec.

Best,
Stefano

[andreaskatis]

Hi Stefano,

Thanks again for your interest in FRET/CoCoSim and the interesting questions you have posed so far. I took some time looking at your example and have a few comments:

• The first two FRET requirements essentially express some expectation over the system inputs. In the Assume-Guarantee paradigm, these should be considered (and treated) as Assumptions. The most recent version of FRET does not export CoCoSpec assumptions, but it is something that we will be adding to the tool very soon. In the meantime, the easiest thing to do would be to edit the generated CoCoSpec/Lustre file, changing the keyword guarantee to assumption for the requirements in question.

• My point above seems to also be solving the issue that you've noticed with the simulation, in combination with the changes that you've made in the second version of the example (System_with_contracts_v2). I ran the simulation with the fixed version of the contract (using assumptions), and the simulation shows that the contract returns false at the fifth second.

Following the above, at the Simulink level, the correct contract should look like the screenshot at the end of this post (you can also manually make these changes at this level, instead of the Lustre level, replacing the "guarantee" blocks for the first two requirements with "Assume" blocks from the CoCoSim Library in Simulink, after you've loaded CoCoSim, of course). The red colored block is the result of a verification task I ran, so you can disregard that detail.

Can you make these changes, and check whether this covers all your intended interactions with CoCoSim?

Best Regards,

Andreas

[andreaskatis]

Hi Stefano,

An important additional note here: It is assumed that in order to properly use the contract block for the purposes of simulation, you have first pre-processed the model with CoCoSim. You can do so by loading CoCoSim, then go to Tools -> CoCoSim -> Extra options -> pre-process this model.