Runtime Verification of Safety-Progress Properties

Abstract. The underlying property, its definition and representation play a major role when monitoring a system. Having a suitable and con-venient framework to express properties is thus a concern for runtime analysis. It is desirable to delineate in this framework the spaces of pro-perties for which runtime verification approaches can be applied to. This paper presents a unified view of runtime verification and enforce-ment of properties in the safety-progress classification. Firstly, we char-acterize the set of properties which can be verified (monitorable proper-ties) and enforced (enforceable properties) at runtime. We propose in particular an alternative definition of “property monitoring ” to the one classically used in this context. Secondly, for the delineated spaces of properties, we obtain specialized verification and enforcement monitors.