Interest beyond violation : on points-of-interest in runtime verification

Abstract

Many formal verification techniques are concerned with comparing system behaviours with formal specifications. Although runtime verification has followed this path (comparing observed traces against formal properties), it has traditionally been burdened with another task—that of raising a flag when a violation is detected. Different approaches can be found in the literature: identifying the earliest such instance, identifying all instances, identifying instances where (potentially future) violations are inevitable, etc. We argue that the lack of a clear distinction between the notion of system correctness and the hard-wired means of identification of points when violation is somehow detected, conflates the notions of points-of-detection and points-of-violation. Frequently, the point at which a point-of-violation may be detected is independent of the point of interest itself, and also independent of the point-of-reaction if a corrective measure is needed. We observe that this distinction becomes more salient in some cases, such as deontic specification languages, which may identify notions such as permission, and in the case of multi-agent systems, where the notion of blame is essential. Using practical and varied examples we motivate why these limitations are significant for the field of runtime verification.