Interest Beyond Violation: On Points-of-Interest in Runtime Verification

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.

1. 1.

   Also note that with this approach, a single trace can have any number of matches.

2. 2.

   Reactions which undo—literally or in some abstract sense—previous system actions due to late monitor detection have been studied in terms of compensations [5].

3. 3.

   We will not use any formal (syntax-specific) notation in the rest of the paper with the exception of regular expressions and Boolean logic connectors. So, we will for instance write globally and finally when referring to LTL formulae; similarly we will write obligation and forbidden instead of using the deontic logic modalities.

4. 4.

   In fairness, one can consider situations in which the detection computation may be deferred for later, e.g., during periods of high load on the system. However, we will only assume online and synchronous runtime verification here.

5. 5.

   We use \(\overline{a}\) to match any event other than a.

6. 6.

   The term contract has been extensively abused to mean different things in computer science, few of which share much with the legal sense of the term. In contrast, here it is being used very much in the sense used in law.

7. 7.

   We assume a time unit granularity of one day.

8. 8.

   A description of this underwater robot scenario is taken from “Monitoring Safety and Reliability of Underwater Robots: A Case Study”, appearing in AISOLA’24 proceedings (through personal communication with the authors).

9. 9.

   This is a simplified version of the specification, with the aim of illustrating our point.

Authors and Affiliations

1. Department of Computer Science, University of Malta, Msida, Malta

   Christian Colombo & Gordon J. Pace

2. Department of Computer Science and Engineering, Chalmers University of Technology and University of Gothenburg, Gothenburg, Sweden

   Gerardo Schneider

Corresponding author

Correspondence to Christian Colombo .

Editors and Affiliations

1. University of Limerick, CSIS and Lero, Limerick, Ireland

   Tiziana Margaria

2. TU Dortmund University, Dortmund, Germany

   Bernhard Steffen

Reprints and permissions

© 2025 The Author(s), under exclusive license to Springer Nature Switzerland AG

Policies and ethics