FRET for hardware resources

[lz3ea]

Hi,
I learned about FRET recently and currently trying to analyze if we should use it.
Something I could not not verify through trial and error is following:

Is it possible to somehow track limited hardware resources like USB Ports?
If I have for example 3 USB Ports in the system and 3 components which USB ports. If I add a fourth component which requires a USB Port I want the realizability check to fail.
Is this possible?

[andreaskatis]

Hi @lz3ea ,

Apologies for a belated response, I only just saw this post.

I am not very familiar with the concept of limited hardware resources, so if there is anything crucial I am missing please elaborate.

The realizability checking analysis is supposed to determine whether, given a set of FRETish requirements, an implementation exists that is guaranteed to always comply to the requirements, no matter what inputs it receives from its environment (think signals, sensor values, etc.).

When you refer to realizability, do you mean the realizability of the system as a whole, containing all 4 components, or the realizability of only the fourth component? The former is not supported in FRET, as we can only analyze one system component at a time.

Despite that, you could maybe describe the system as a monolithic component, where each of the underlying submodules is uniquely defined through its own variables. In that case, I believe that it would be possible to describe a scenario where, the fourth component is supposed to take control of the limited resource, but it cannot do so due to some other requirement(s) dictating that, at the same time point, another submodule requires the same resource.

Assuming that you want to look into this further, please keep in mind that currently our realizability analysis is limited only to safety requirements. As such, any form of liveness in your specification may result in unsound results.

Let us know if you have any further questions! An example could go a long way in order for us to further understand your use case too.

Best Regards,

Andreas