Verifying Total Sojourn Time in a Specific State in UPPAAL

[Szpilman2]

Dear UPPAAL Team,

I hope this message finds you well.

I have two timed automata named "Software" and "Hardware". I have attached pictures of the models.
software:

hardware:

Whenever the Software TA sends a signal through the "use" channel, the Hardware TA receives the signal and transitions to the "using" state. The Hardware remains in the "using" state (in my case 2 units of time) for a short period before transitioning to the "tail" state.

I would like to write a query that verifies whether the total time the Hardware spends in the "tail" state (accumulated over all instances of "use?" in the Software TA) is less than a certain constant. I am unsure how to write this query. My initial approach was to save the clock values, but I understand that this is not possible in UPPAAL.

In other words, I need to check if the sum of the sojourn times in the "tail" state is less than a specific constant.

I have also attached my model for your reference.
EnergyHotspotModel.zip

Thank you very much for your assistance.

Best regards,
-- Peyman

[mikucionisaau]

To extract the maximum time spent in Tail, try the supremum query:

sup{hardware.tail}: clk

To compute the cumulative duration, please add a stop watch, e.g. sw: a clock whose progress is stopped with sw'==0 expression in the invariant (add such invariant to all locations of hardware except Tail) and then use the supremum query over sw.

Note that with stop watches the symbolic analysis becomes over-approximate (UPPAAL may start issuing maybe verdicts to certain queries), but in such case it's most likely still exact (I don't have a proof) as it does not disturb the logic of the model (model does not use constraints over sw).

See the publication about stopwatches: https://doi.org/10.1007/3-540-44618-4_12

[Szpilman2]

thank you so much. your answers are life saving.
you mean to say I define hybrid clock sw in HardwareModel declarations and add this to all location of hardware except Tail like this?

now my question is some locations like Using has invariant like clk <= D_Use && sw' == 0 and I think it is not correct. in other words adding sw to the invariants affects my original invariant in the model. how can I figure this out?

also is sup{}:sw correct query for my property?

[mikucionisaau]

Did you declare the sw?
You need to have a line in global declarations, like:

clock sw;

[Szpilman2]

no no I did not define it in global declaration I had defined it in declarations for Hardware TA.
now it's my result. UPPAAL says that the property may be satisfied and returns 16 as result of the query.

now how can I compare result of sup sw with specific constant in another query?

Marius you are my hero man. Thank you so much.

[Szpilman2]

also I will check the publications thanks for sharing.

[mikucionisaau]

If you define sw locally in hardware then you can refer to it by hardware.sw just like any variable.