Evolution since "The Ten Lockheed Martin Cyber-Physical Challenges: Formalized, Analyzed, and Explained"

[simtheverse]

Hello, I am checking out this paper: The Ten Lockheed Martin Cyber-Physical Challenges: Formalized, Analyzed, and Explained

In Section VI Lessons Learned, it says:

Can LMCPS requirements be captured in FRET?
We captured 69 out of 74 LMCPS requirements in FRET. As mentioned, we were not able to formalize requirement [TUI-004] that contains a temporal condition. Additionally, several requirements refer to the previous value of a variable (e.g., see [AP-003c-v4]), defined in pmLTL with the Y operator, in Lustre with the pre operator, and in Simulink as a delay block. Currently, F R E T I S H cannot express ‘previous value of a variable’. To shortcut this limitation, we used internal/auxiliary variables which we defined at the COCOSPEC level, but a FRETISH solution would be desirable.

I was curious if FRET has grown to handle any of the conditions that prevented FRET from being used above?

[anmavrid]

Hello @simtheverse,

Thank you for your excellent question!

Yes, we have extended the expressiveness of FRETish:

• We have added temporal conditions;
• We have also added functions that support expressing "previous value of a variable".

See detailed explanations here: https://github.com/NASA-SW-VnV/fret/blob/master/fret-electron/docs/_media/user-interface/examples/temporal_condition_explanations.md

Thanks,
Anastasia

[simtheverse]

Awesome, thank you!