Deadlock and livelock

This lesson explains the concepts of deadlock and livelock.

Deadlock

If no event transitions are possible, and also no time transitions are possible (time may not progress), then no transitions are possible. This is called deadlock. No behavior is possible, or will ever become possible. As an example, consider the following CIF specification:

automaton use_case:
  location wait3:
    initial;
    urgent;
    edge tau when time > 3 goto done;

  location done;
end

Location wait3 is the initial location. Initially, time is zero. Time can not progress, as the location is urgent. Since the guard of the edge also does not hold, event tau is also not possible. No transitions are possible, and the specification is in deadlock.

Livelock

As long as an event is possible, no time may pass. If by mistake always an event is possible, this prevents all passage of time. Consider the following CIF specification:

automaton car:
  event increase, decrease, arrived;
  disc real speed = 0;
  cont pos = 0 der speed;

  location underway:
    initial;
    edge increase when speed < 100 do speed := speed + 1;
    edge decrease when speed > 0   do speed := speed - 1;
    edge arrived  when pos = 850 goto done;

  location done;
end

This specification models a car that can increase and decrease its speed, so that it is at least 0 and at most 100. It keeps track of its position (continuous variable pos) that increases more quickly as the speed increases. When position 850 is reached, the car has arrived and is done.

The car will be increasing and decreasing it speed, using the increase and decrease events. As always at least one of them is enabled at any moment, time can never progress, and pos remains zero. This effect is called livelock. While behavior is still possible, the model does not truly progress with useful behavior. The model gets 'stuck' repeating one or a few events.