We’re here to help you


Using 'external'

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.


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


1 Communication over 'port' is possibly delayed.


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();

    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;

    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;

If you have questions that weren’t answered by this Guide,
let our support team help you out.

Enjoy this article? Don't forget to share.