comparing stopwatch clock value in UPPAAL

[Szpilman2]

Dear UPPAAL Team,

I hope this message finds you well.

I have two questions:

1. In the following timed automata model, I have a stopwatch clock. Is it possible to compare the value of the stopwatch clock with a constant or another clock? For instance, I want to compare the value of the stopwatch clock with a specific constant like 4. Whenever the value of the stopwatch clock exceeds this constant, I want the automaton to transition to another location. In other words, is it possible to compare the value of the stopwatch clock on the edge of the timed automata?
   

2. Suppose we have two components, each with a specific clock rate, and we want to model them using timed automata. For example, I want to model software running on a fast CPU and embedded hardware operating slower than the CPU. (I want to model both software and embedded hardware specification as Timed Automata) These components should communicate with each other via channels. My question is whether channels are suitable for modeling this scenario, and if there is any related work that addresses a similar situation. (my embedded hardware is a I/O device and the software sends instruction to the hardware. and I suppose that using I/O device in software is blocking, in other words the software gets blocked and waits until I/O operation is completed.)

Thank you so much.

Best regards,
Peyman

[mikucionisaau]

1. Yes, stopwatches can be used the same as any other clock. It's only reachability analysis becomes over-approximate: if UPPAAL says that some state is not reachable, then it is for sure reachable. Alternatively UPPAAL will say "maybe satisfies" which indicates that the found trace may be spurious.

2. Yes. Actually synchronization through channels is a preferred method as opposed to asynchronous read/write of shared variables which result in much larger state spaces, which is harder to analyse. You need to guarantee the assumption that signal transport time is negligible, i.e. effectively zero. So it all depends on the assumption one can make, how realistic they are.