Runtime Verification Logics A Language Design Perspective

Runtime Verification is a light-weight approach to systems verification,
where actual executions of a system are processed and analyzed using rigorous
techniques. In this paper we shall narrow the term’s definition to represent the
commonly studied variant consisting of verifying that a single system execution
conforms to a specification written in a formal specification language. Runtime
verification (in this sense) can be used for writing test oracles during testing when
the system is too complex for full formal verification, or it can be used during deployment
of the system as part of a fault protection strategy, where corrective
actions may be taken in case the specification is violated. Specification languages
for runtime verification appear to differ from for example temporal logics applied
in model checking, in part due to the focus on monitoring of events that carry
data, and specifically due to the desire to relate data values existing at different
time points, resulting in new challenges in both the complexity of the monitoring
approach and the expressiveness of languages. Over the recent years, numerous
runtime verification specification languages have emerged, each with its different
features and levels of expressiveness and usability. This paper presents an
overview and a discussion of this design space.