Software Tools for Technology Transfer manuscript No. (will be inserted by the editor) What can you Verify and Enforce at Runtime?

Abstract. The underlying property, its definition and representation play a major role when monitoring a sys-tem. Having a suitable and convenient framework to ex-press properties is thus a concern for runtime analysis. It is desirable to delineate in this framework the sets of properties for which runtime analysis approaches can be applied to. This paper presents a unified view of runtime verifica-tion and enforcement of properties in the Safety-Progress classification. Firstly, we extend the Safety-Progress clas-sification of properties in a runtime context. Secondly, we characterize the set of properties which can be veri-fied (monitorable properties) and enforced (enforceable properties) at runtime. We propose in particular an al-ternative definition of “property monitoring ” to the one classically used in this context. Finally, for the delineated sets of properties, we define specialized verification and enforcement monitors.