Interface Contracts (Dezyne Reference Manual)

7.1 Interface Contracts

Dezyne does not have an exception mechanism like other languages. An exception mechanism is designed to prevent accidentally ignoring missed pre- or post-conditions. Instead, in Dezyne the interfaces establish these restrictions by means of verification (See Formal Verification). So where traditional programming languages must handle protocol violations using an exception mechanism at runtime, Dezyne prevents them using the static verification checks⁷. Interfaces in Dezyne are inherently complete with respect to their event alphabet. The generated code will accept every trigger but give an illegal response.

The illegal response is mapped to std::abort () in C++. Note that for a fully verified Dezyne system, operated by clients that adhere to the interface specifications, it is impossible for an illegal response to be triggered. In other words, when an illegal is triggered, it means that some non-Dezyne code is violating a protocol (interface specification).

Implicit interface constraints
Shared interface variables

7.1.1 Implicit interface constraints

Dezyne version 2.17.0 introduces implicit interface constraints.

Before 2.17.0, for a component to be compliant with its provides interface(s), implementing a component required meticulously specifying the same behavior in the component as in the provides interface(s); therefore the code from the interface(s) is often repeated in the component.

Since version 2.17.0 the provides interface(s) are implicitly applied as a constraint on the component behavior. This means that anything disallowed by the interface, i.e., explicitly or implicitly marked as illegal, is implicitly marked as illegal in the component behavior.

How does this differ from the existing implicit illegal feature See illegal you may wonder. The implicit illegal feature leads to implicitly marked illegal behavior when a certain event is ommitted in a certain state. The constraint feature marks as illegal every event in the component behavior which is marked as illegal in the corresponding state in the interface behavior. This avoids the need to repeat the state and guarding from the interface in the component. An example of how this may reduce the behavior specification of a component is the component proxy.

7.1.2 Shared interface variables

Dezyne version 2.18.0 introduces shared interface variables.

Before 2.18.0, for a component to be able to act on the state of another component through a guard, if or reply expression, it was necessary to define and maintain a shadow copy of said state, either by inferring its value or explicitly retrieving it via an action.

Now, components on either side of an interface can use and share the value of their interface state variables by referring to them via their respective ports in any expression.

port.variable.

Note: Access is limited to reading only, assignments from the component behavior are prohibited. Also, variables from ports marked external are inaccessible, due to the process delay between both sides of the interface.

Note: Shared interface variables are not inspected by defer. As a consequence an explicit component variable that changes state is required to cancel a defer, see Component defer for more information.

Shared interface state further enhances an existing Dezyne pattern, where an assert event combined with a predicate guarding an illegal is used to define a user defined functional property across multiple components. An example of this is used by the cruise_control example below. Here the cruise_control explicitly checks for unwanted acceleration due to not resetting the throttle or forgetting to stop the timer, as well as the converse property.

interface ihmi
{
  in void enable ();
  in void disable ();

  in bool set ();
  in bool resume ();
  in void cancel ();

  out void inactive ();

  behavior
  {
    enum State {Disabled,Enabled,Active};
    enum Setpoint {Unset,Set};

    State state = State.Disabled;
    Setpoint setpoint = Setpoint.Unset;

    on disable: // always allow
    {
      state = State.Disabled;
      setpoint = Setpoint.Unset; //forget about the previous setpoint
    }

    [!state.Disabled] on enable: {/* ignore when not disabled */}
    [!state.Active] on cancel: {/* ignore when not active */}
    [!state.Enabled] on set, resume: reply (false);

    [state.Disabled] on enable: state = State.Enabled;
    [state.Enabled] {
      on set, resume: reply (false);
      on set: {state = State.Active; setpoint = Setpoint.Set; reply (true);}
      on resume: {
        [setpoint.Set] {state = State.Active; reply (true);}
        [setpoint.Unset] reply (false);
      }
    }
    [state.Active]
    {
      // this may or may not happen
      on inevitable: {state = State.Enabled; inactive;}
      on cancel: state = State.Enabled;
    }
  }
}

// observe (brake and clutch) pedals
interface ipedals
{
  in bool enable ();
  in void disable ();
  out void engage ();
  out void disengage ();
  behavior
  {
    bool monitor = false;
    bool engaged = false;
    [!monitor] {
      on enable: {monitor = true; reply (engaged);}
      on enable: {monitor = true; engaged = !engaged; reply (engaged);}
    }
    [monitor] {
      on disable: {monitor = false; engaged = false;}
      on optional: {
        engaged = !engaged;
        if (engaged) engage; else disengage;
      }
    }
  }
}

// interface to the throttle actuator PID control
interface ithrottle
{
  in void setpoint ();    // close loop and calculate actuator input
  in void reset ();  // open loop
  out void unset (); // sponaneous open loop

  behavior
  {
    bool active = false;
    on setpoint: active = true;
    [active] {
      on reset: active = false;
      on optional: {active = false; unset;}
    }
  }
}

interface itimer
{
  in void start ();
  out void timeout ();
  in void cancel ();
  behavior
  {
    bool idle = true;
    [idle] on start: idle = false;
    [!idle] on inevitable: timeout;
    on cancel: idle = true;
  }
}

interface iassert
{
  out void assert ();
  behavior
  {
    on inevitable: assert;
  }
}

import cruise-control-interfaces.dzn;

component cruise_control
{
  provides ihmi hmi;
  requires ipedals pedals;
  requires ithrottle throttle;
  requires itimer timer;
  requires iassert check;
  behavior
  {
    // functional property that asserts no unwanted acceleration
    on check.assert (): {
      [!hmi.state.Active] {
        [throttle.active] illegal;
        [!timer.idle] illegal;
        [otherwise] {}
      }
      [otherwise] {
        [!throttle.active] illegal;
        [timer.idle] illegal;
        [otherwise] {}
      }
    }
    [hmi.state.Disabled] {
      on hmi.enable (): bool b = pedals.enable ();
      on hmi.disable (): {}
    }
    [!hmi.state.Disabled] {
      on hmi.enable (): {}
      on hmi.disable (): {
        if (throttle.active) throttle.reset ();
        timer.cancel ();
        pedals.disable ();
      }
    }
    [hmi.state.Enabled && timer.idle] {
      [pedals.engaged] on hmi.set (): reply (false);
      [!pedals.engaged] on hmi.set (): {
        throttle.setpoint ();
        timer.start ();
        reply (true);
      }
      on hmi.resume (): {
        [pedals.engaged || !hmi.setpoint.Set] reply (false);
        [otherwise] {
          throttle.setpoint ();
          timer.start ();
          reply (true);
        }
      }
    }
    [!hmi.state.Enabled || !timer.idle] {
      on hmi.set (), hmi.resume (): reply (false);
    }
    on timer.timeout (): {
      if (!hmi.state.Active) illegal;
      throttle.setpoint ();
    }
    on hmi.cancel (): {
      if (hmi.state.Active) {
        throttle.reset ();
        timer.cancel ();
      }
    }
    on pedals.disengage (): {/*ignore*/}
    on pedals.engage ()
      , throttle.unset (): {
      if (hmi.state.Active) {
        hmi.inactive ();
        timer.cancel ();
        if (throttle.active) throttle.reset ();
      }
    }
  }
}

Note: This Dezyne pattern is intended to become a first class citizen in the Dezyne language when the Module model type is added.

7.1 Interface Contracts

7.1.1 Implicit interface constraints

7.1.2 Shared interface variables

Footnotes

(7)