Menu

since 2.0.0

The 'external' keyword specifies that communication over a port may be delayed. (The delay may be caused by inter-process communication.) Model verification will consider this delay for out events on an external port. The delay may cause race conditions leading to illegal behaviour or interface compliance errors.

'external' delay is taken into account for required port out events. Marking a provided port as external has no effect on verification.

Syntax

requires external Interface port; (Since 2.0.0) (1)
provides external Interface port; (Since 2.0.0) (1)

Explanation:

1 Communication over 'port' is possibly delayed.

Examples

Race condition due to external delay

Component RemoteTimerProxy illustrates how a delayed communication channel may cause a race condition leading to illegal behaviour.

The implementation of component RemoteTimerProxy is correct for 'requires ITimer rp' but incorrect for 'requires external ITimer rp' due to race between pp.cancel and rp.timeout.

extern double $double$;

interface ITimer
{
  in void create(double seconds);
  in void cancel();
  out void timeout();

  behaviour
  {
    bool is_armed = false;

    [!is_armed] on create: is_armed = true;
    [is_armed] on create: illegal;

    on cancel: is_armed = false;

    [is_armed] on inevitable: {timeout; is_armed = false;}
  }
}

component RemoteTimerProxy {
  provides ITimer pp;
  requires external ITimer rp;

  behaviour
  {
    bool is_armed = false;

    on pp.create(s):
    {
      [!is_armed] {rp.create(s); is_armed = true;}
      [is_armed] illegal;
    }

    on pp.cancel(): {rp.cancel(); is_armed = false;}

    on rp.timeout():
    {
      [is_armed] {pp.timeout(); is_armed = false;}
      [!is_armed] illegal;
    }
  }
}

See also:

Enjoy this article? Don't forget to share.