Bounded response check

The controller properties checker can check a supervisor for having bounded response.

The bounded response property holds if for each execution of the code, the number of transitions to execute for uncontrollable and controllable events are both bounded. This property ensures that the code that executes the uncontrollable events, as well as the code that executes the controllable events, always terminate. That is, the system has no loops with only uncontrollable events, or with only controllable events. In other words, there is no livelock for uncontrollable events, nor for controllable events.

Examples

The check verifies lack of transition loops that consist of only uncontrollable or only controllable events. For example, the Actuator automaton in the example below has bounded response, because between transitions for events c_on and c_off, the location of Sensor has to change via an uncontrollable event. The Sensor automaton does not have bounded response, as the sensor can keep go on and off forever, without restrictions.

plant Actuator:
  controllable c_on, c_off;

  location Off:
    initial;
    edge c_on when Sensor.On goto On;
  location On:
    edge c_off when Sensor.Off goto Off;
end

plant Sensor:
  uncontrollable u_on, u_off;

  location Off:
    initial;
    edge u_on goto On;
  location On:
    edge u_off goto Off;
end

The model below also does not have bounded response. Whenever StartButton and StopButton are both equal to true, the motor keeps starting and stopping.

input bool StartButton, StopButton;

plant Motor:
  controllable c_on, c_off;

  location Off:
    initial;
    edge c_on when StartButton goto On;
  location On:
    edge c_off when StopButton goto Off;
end

Implementation details

Bounded response for a model is determined as follows:

  • Compute the reachable states (R0) of the system.

    Transitions for all events are considered. Input variables can also change their value to any other value, at any time.

  • Compute the bound for the uncontrollable events.

  • Compute the bound for the controllable events.

Given the reachable states, computing a bound is done as follows:

  1. If there are no reachable states, the system can’t be initialized, and the bound is zero.

  2. The reachable states R0 are the states that can be reached after applying zero transitions from any reachable state.

  3. Take all possible transitions from states in R0. The resulting states are the states reachable with one transition from the states in R0, and we call these states R1.

  4. Take all possible transitions from states in R1. The resulting states are the states reachable with two transitions from the states in R0, and we call these states R2.

  5. And so on, to compute R3, R4, etc.

  6. If the specification has bounded response, then some Rx will be an empty set of states, as no more transitions are possible. The bound is x - 1, since no states could be reached with x transitions from R0, while there are states that could be reached with x - 1 transitions from R0.

  7. If the specification does not have bounded response, it has at least one cycle of states. The states within a cycle will with one transition go to the next state in their cycle. Cycles are thus preserved with each step. If all bounded sequences at some point end, then only the cycles remain. Then a fixed point will be reached (Rx and Ry with x + 1 = y are the same set of states) and there is no bounded response.