Fret to Simulink A/G Contract

[StefanoCentomo]

The abstraction level of FRETish language is really interesting and more suitable for engineers that are not familiar with temporal logic formalization.

I have a couple of questions regarding FRETish, coupled with CoCoSim.
In particular, related to the "Bridging the Gap Between Requirements and Simulink Model Analysis" paper.

I'm interested in the generation of simulink monitors starting from FRETish.

1. Does FRETish generates also Assume/Guarantee Contracts in LTL/pmLTL?

2. Does CoCoSim generate only the contract skeleton or synthesize also the implementation?

3. I've tried to export some simple requirements in CoCospec but I didn't find any Lustre-to-CoCoSim importer.
   How can I import the cocospec zip archive into CoCoSim?

Thanks a lot!
Steve

[anmavrid]

Hi Steve,

Thanks for your interest in the FRET and CoCoSim tools! Here are my answers:

1. Yes, it does generate contracts in CoCoSpec code (with the LTL/pmLTL expressions being added as assumptions or guarantees). As an example, I have attached the assume/guarantee contract that FRET generates for the FRETDemo requirements.
   FSMCoCoSpec.zip

2. CoCoSim synthesizes the full requirements, i.e., the complete CoCoSpec specification, and not just the contract skeleton.

3. To import the cocospec zip file in CoCoSim, you need to Click on Tools > CoCoSim > Requirements > Import Requirements. See screenshot below:

Is this helpful?

Thanks,
Anastasia

[StefanoCentomo]

Thank You for your quick and clear answer!

I finally found everything, but I have still some issues.

In particular, I've tried this simple requirement, without any mode or temporal constraint:

The aircraft shall always satisfy airspeed >= 100.0

I have mapped airspeed as a double with output causality.

I exported the mapped req with CocoSpec without coupling any model.

I've installed lustrec and put all the executables in the Cocosim specific folder.

Anyway, lustrec returns this error:

parsing source file ./aircraftSpec.lus
Syntax error: Impossible to parse the following node specification:
contract aircraftSpec () returns (airspeed: real; );

let
var FTP: bool = true -> false;
(* Req text: the aircraft shall always satisfy airspeed >= 100.0 *)
guarantee "1" (H((airspeed >= 100.0)));
tel
File "./aircraftSpec.lus", line 138, characters 23-24:

Here, you can find the lus file generated by fret.
aircraftSpec.zip

i'm using fret v2.6 on a ubuntu 22.04.

Do you have any hint or suggestion?

Thanks!
Steve

[andreaskatis]

Hi @StefanoCentomo ,

This is related to an issue with LustreC not accepting nodes with no inputs. We are currently looking into addressing this in FRET. For the time being, you can avoid this issue by introducing an input variable, either through a FRET requirement (also designating it as input in variable mapping), or by editing the node containing the FRET requirements in the resulting .lus file.

For the latter, you'd need to open the .lus file, and change line 138 from

(*@contract aircraftSpec () returns (airspeed: real; );

to

(*@contract aircraftSpec (tempIn: bool) returns (airspeed: real; ); (i.e. introducing the tempIn input variable.

Best Regards,

Andreas

[StefanoCentomo]

Thank you Andreas,
it is working.

I have another (hopefully last) question related to this issue.

I have a simple Simulink model with 2 inputs (in_1 and in_2) and one output (out).

I have defined these three following requirements:

Component shall always satisfy in_1 > 0.0
Component shall always satisfy in_2 > 0.0
Component shall always satisfy out > 5.0

Then, I have connected the requirements with the Simulink Model through the variable mapping.

In this case, I have generated the Contract block that correctly synthesized those requirements.

I have changed the third requirement into:

if out < 5.0 Component shall within 5 seconds satisfy out > 5.0

When I try to import the Requirements, Cocosim returns the following errors:

(Error)[generate_lusi] generation of lusi file failed for file "ComponentSpec"
(Error)[TOLUSTRE] Lustre Syntax check has failed for contract code. The parsing error is the following:
(Error)[TOLUSTRE] .. parsing source file ComponentSpec
Syntax error: Impossible to parse the following node specification:
contract ComponentSpec (in_1:real; in_2:real; ) returns (out: real; );
let
var FTP: bool = true -> false;
(* Req text: Component shall always satisfy in_1 > 0.0 )
guarantee "1" (H((in_1 > 0.0)));
( Req text: Component shall always satisfy in_2 > 0.0 )
guarantee "2" (H((in_2 > 0.0)));
( Req text: if out < 5.0 Component shall within 5 seconds satisfy out > 5.0 *)
guarantee "3" (H((OT(5,5,(((out < 5.0) and ((YtoPre( not (out < 5.0))) or __FTP)) and ( not (out > 5.0))))) => (OT(5-1,0,(__FTP or (out > 5.0))))));
tel
File "ComponentSpec", line 184, characters 116-118:

Here you can find the zip file from FRET related to this test.
Component2.zip

Is it the same problem with the previous example?
In this case, globally, I have defined two inputs and one output, but they are not coupled in the same requirement.

From FRET-User perspective, Do I have to define an input (or a mode) in the output requirement and rephrase it?

Best,
Stefano

[andreaskatis]

Hi Stefano,

Looking at the new file, there are two issues that we have a fix for in the works. First of all FTP is defined as a variable but __FTP is used in the requirement definitions. You'd need to edit the file so that either FTP or __FTP is used within the ComponentSpec node.

The second issue is again related to LustreC. The first argument of the second call to node OT in guarantee 3 appears to be 5-1 . This is not properly parsed by LustreC. To resolve it, either replace the expression by the resulting value (in this case the number 4) or by adding spaces before and after the subraction (i.e. change the expression to 5 - 1).

Best Regards,

Andreas

[anmavrid]

Hi @StefanoCentomo,

There was a question here that @andreaskatis correctly pointed out that it is more related to the CoCoSim tool.

However, if there is a question about how to capture periodic behaviors in FRETish requirements (that can be subsequently translated into CoCoSim monitors), here is a relevant discussion: #51.

Anastasia

[StefanoCentomo]

Hi Anastasia,
Thank you for your answer.

The question is more related to the internal time-evolution of the Monitor.

I have opened a topic in CoCosim discussion section regarding this point, with a simple Simulink example: #14.

I think that point could also affect Fret, in particular the translation phase from Fretish to CoCoSpec.

Best,
Stefano