I'd like to learn more about Timed Automata to verify real-time systems. Currently, I'm trying to get myself familiar with a tool called UPPAAL.
I drew some simple graphs and added different properties. The entire model is supposed to represent a production cell system where different mechanical units pass a block to each other.
I've modelled the block (BlockCycle), 2 mechanical units (Feeder, FeederBelt) and 2 sensors which sense the arrival of the block.
Even though I thought my system would make sense, it gets deadlocked:
The target states of this transition violate the invariants. This is not a problem, as long as you intended your model to behave like this.
(No I didn't. ;P)
I can't seem to find the reason for the deadlock, though. The tool points me to the BlockCycle model but I didn't specify any invariant there. In fact, all the transition requirements are fulfilled so the transition (from Pos7 to Pos8) should definitely be taken.
Below you'll see how the systems evolves and finally gets stuck (error message pops up).
Labels:
- green : property check (e.g. FB_Running means FB_Running == true )
- dark blue: property updates/assignments
- dark red: locations (e.g. Pos7 or Pos8)
The BlockCycle model with the respective transition in question:
My Question: Why does the system deadlock even though there are still transaction which could be taken.
Edit1: When I remove the invariant property of Sensor7's location Active (called BlockAtPos[7]) the deadlock is resolved. So I guess, since there is no synchronization between Sensor7 and BlockCycle for the last transition before it deadlocks, that would cause to a contradiction (BlockAtPos[7] becoming false while the sensor has not yet the chance to take the InActive transition) and thus violating the invariant.
Note: You can find my UPPAAL code/file here: pcs.xml.