Ylies Falcone, Jean-Claude Fernandez, Laurent Mounier
What Can You Verify and Enforce at Runtime? (2010)
What Can You Verify and Enforce at Runtime? (2010)
TR-2010-5.pdf
Keywords: runtime verification, runtime enforcement, safety-progress classification, monitorability, enforceability, monitor synthesis
Abstract: The underlying property, its definition and representation play a major role when monitoring a system. Having a suitable and convenient framework to express properties is thus a concern for runtime analysis. It is desirable to delineate in this framework the spaces of properties for which runtime analysis approaches can be applied to. This paper presents a unified view of runtime verification and enforcement of properties in the Safety-Progress classification. Firstly, we extend the Safety-Progress classification of properties in a runtime context. Secondly, we characterize the set of properties which can be verified (monitorable properties) and enforced (enforceable properties) at runtime. We propose in particular an alternative definition of ``property monitoring'' to the one classically used in this context. Finally, for the delineated spaces of properties, we obtain specialized verification and enforcement monitors.
