This is a new one on me.

It raises an interesting question, though: how do you incorporate performance requirements (tolerance levels, etc) into formal specifications? Especially as these will presumably depend on the computing power of the hardware system the specification is implemented on.

I find that the Jasper online Sinclair ZX Spectrum Java emulator suffers from the reverse of this - what we might call the hyperactive gerbils problem. It just runs too damn fast for any of the games on it to be playable (apart from Chaos).

I can imagine a solution where you synchronize with an internal clock, and guarantee a) that an operation will complete before the next clock tick, or throw some exception, and b) that the subsequent operation will not begin until after then next clock tick. Then the work rate of the gerbils would be strictly controlled.