Question regarding the FRETish Grammar for periodically events

[ghost]

Hello all,

I was wondering how the following Rationale could be formulated as FRETish style requirement.

Rationale: When an over-voltage error occurs the system shall broadcast an error message, every 2 seconds.

Can you maybe give me a hint on how the FRETish styled requirement could look like?

Cheers.

[anmavrid]

Hi @FlorianGuhl-zeiss,

Thanks for the question. One way to do it is with the following three requirements:

1. Upon overvoltage the sw shall immediately satisfy error_message.

2. Upon error_message the sw shall after 1 second satisfy aux_state.

3. Upon aux_state the sw shall after 1 second satisfy error_message.

The aux_state is just an auxiliary variable I am using to enforce the periodical behavior.

Anastasia

[anmavrid]

Another way is to use the following two requirements:

1. Upon overvoltage the sw shall immediately satisfy error_message
2. Upon error_message the sw shall at the next timepoint satisfy occurs(1,error_message) & !error_message

for infinite trace. For finite trace (e.g., if you want to use the FRET simulator) the second requirement must be written with LAST (last time point of the trace) as follows:

Upon error_message the sw shall at the next timepoint satisfy LAST | (occurs(1,error_message) & !error_message)

Thanks for the interesting question! Please do let us know if something is not clear.

The semantics of occurs is explained in the FRET manual.

Anastasia

[ghost]

Hello @anmavrid,
thank you for your detailed answer. Solution 1. is to me more understandable out of the box. For solution 2. or in general with FRETish, I currently tend to not use timepoints. Because the term seems vague to me, but this would be another question/topic.

Thank you again for your quick response!