Vacuous real-time requirements

We introduce the property of vacuity for requirements. A requirement is vacuous in a set of requirements if it is equivalent to a simpler requirement in the context of the other requirements. For example, the requirement “if A then B” is vacuous together with the requirement “not A”. The existence of a vacuous requirement is likely to indicate an error. We give an algorithm that proves the absence of this kind of error for real-time requirements. A case study in an industrial context demonstrates the practical potential of the algorithm.