Previous: , Up: Individual Armour cases   [Contents]


7.3.9 ArmourREIR (RangeErrorInRequiresReply)

The reply of a requires interface event could have a range error (a mis-mapping between two subints). The system diagram shows the armour at the requires port of the Dezyne component:

ArmourREIR

We only deal with one in-event areturning an integer value. We defined 2 integer ranges. The Strict interface use the most restricted one so we only allow a very limited set of reply values.

interface IStrict
{
  in SubCount ia();

  behaviour
  {
    SubCount c=0;
    on ia: reply(0);
    on ia: reply(1);
    on ia: reply(2);
  }
}

The Robust interface allows the more relaxed set of reply values. In the model code we do not have to describe all possible reply values as long as we at least define one good case and one bad case that the verifer can investigate.

interface IRobust
{
  in AllCount ia();

  behaviour
  {
    on ia: reply (-1);  // -1 triggers an error
    on ia: reply (0);   // 0 is ok behaviour
  }
}

In the armour an in-event at the provides port is passed to the requires port. If the reply value from the requires port is outside the strict range it is logged as an error and either the lower or upper boundary of the restricted range is returned.

component ArmourREIR // IStrict to IRobust
{
  provides IStrict pStrict;
  requires IRobust rRobust;
  requires injected ILogger iLog;

  behaviour {
    AllCount c = 0;

    on pStrict.ia(): {
        c = rRobust.ia();
        if (c<0) {
            iLog.Log($"Reply value from ia outside range (too small)"$);
            reply(0);
        }
        else if (c>2) {
            iLog.Log($"Reply value from ia outside range (too large)"$);
            reply (2);
        }
        else reply(c+0);
    } // armour on boundary values
  }
}

The full armour example code including the client and overall system component is here:

Basic example: ArmourREIR
Example with error handling: ArmourREIRError


Previous: , Up: Individual Armour cases   [Contents]