Safety Property: SoftSendLimit

property SoftSendLimit (limit: int, tq: int) {
    // Limit network bandwidth useage to limit bytes nbytes every timeStep (in milliseconds)
    // Soft limit means that  where possible network communication is slowed
    // down to match the limit, rather than terminating the program.
    requires SoftSendCounterNetConnectionNames;
    useinterface java.net.Socket: java.net.RegulatedSendSocket,
        java.net.DatagramSocket: java.net.RegulatedSendDatagramSocket;
    
    check RNetwork.initialize () {
        timeQuantum = tq;
        sendLimit = limit;
    }
    
    precode RNetwork.preSend (remote: RNetAddress, nbytes: int) {
        util.Assert.assert (nbytes + bytesSent <= sendLimit); 
    }
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science