Please use this identifier to cite or link to this item:
Title: An operational guide to monitorability with applications to regular properties
Authors: Aceto, Luca
Achilleos, Antonis
Francalanza, Adrian
Ingólfsdóttir, Anna
Lehtinen, Karoliina
Keywords: Computer software -- Verification
Object monitors (Computer software)
Computer logic
Software engineering
Issue Date: 2021
Publisher: Springer-Verlag
Citation: Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., & Lehtinen, K. (2021). An operational guide to monitorability with applications to regular properties. Software and Systems Modeling, 20(2), 335-361.
Abstract: Monitorability underpins the technique of runtime verification because it delineates what properties can be verified at runtime. Although many monitorability definitions exist, few are defined explicitly in terms of the operational guarantees provided by monitors, i.e. the computational entities carrying out the verification. We view monitorability as a spectrum, where the fewer guarantees that are required of monitors, the more properties become monitorable. Accordingly, we present a monitorability hierarchy based on this trade-off. For regular specifications, we give syntactic characterisations in Hennessy–Milner logic with recursion for its levels. Finally, we map existing monitorability definitions into our hierarchy. Hence, our work gives a unified framework that makes the operational assumptions and guarantees of each definition explicit. This provides a rigorous foundation that can inform design choices and correctness claims for runtime verification tools.
Appears in Collections:Scholarly Works - FacICTCS

Files in This Item:
File Description SizeFormat 
An operational guide to monitorability.pdf
  Restricted Access
776.14 kBAdobe PDFView/Open Request a copy

Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.