Performance and verification

Some twentyfive years ago, the field of computer-communication system performance evaluation and the field of formal specification and verification were regarded as completely disjunct. The former field focussed on the quantitative aspects of system behaviour, expressed in measures such as delays, throughputs and loss probabilities, whereas the latter field focussed on the qualitative aspects of system behaviour, expressed in measures (or, properties) such as system liveness, deadlock freeness and safety. Over the years, however, this distinction has shown to be not always useful. In fact, we see a large variety of systems for which the qualitative behaviour cannot be decoupled from the quantitative aspect. Think for instance of communication protocols in an embedded system setting: the qualitative correctness of a protocol, without considering (absolute) timing aspects, is not enough for classifying a protocol as correct. Indeed, only when the protocol behaves as it should, and does so in a timely manner, the protocol can be regarded as correct. Observations of this kind have lead to a variety of integrated approaches toward performance evaluation and verification