Safety Property: NetHardReceiveBandwidthLimit

property NetHardReceiveBandwidthLimit (bLimit: int, tLimit: int) {
  // Limit network bandwidth useage to nbytes every timeStep (in milliseconds)
  // Hard limit means that an error is reported whenever the limit is
  // exceeded.
  requires NetworkReceiveBandwidthCounter;

  postcode RNetwork.initialize () {
    receiveTimeSlice = tLimit;
    receiveByteLimit = bLimit;
    receiveBytesLeft = bLimit;
  }
  
  check RNetwork.preReceive (remote: RNetADdress, nbytes: int) {
    NetHardBandwidthLimitCheck (nbytes, receiveBytesLeft, receiveByteLimit,
                                receiveTimeSlice, "receive"); 
  }
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science