Towards Partial Monitoring: It is Always too Soon to Give Up
This addresses a limitation in formal verification for system developers, though it appears incremental as it builds on existing monitorability concepts.
The paper tackles the problem of non-monitorable properties in runtime verification by proposing partial monitors that can partially check these properties, showing how they can be used in practice.
Runtime Verification is a lightweight formal verification technique. It is used to verify at runtime whether the system under analysis behaves as expected. The expected behaviour is usually formally specified by means of properties, which are used to automatically synthesise monitors. A monitor is a device that, given a sequence of events representing a system execution, returns a verdict symbolising the satisfaction or violation of the formal property. Properties that can (resp. cannot) be verified at runtime by a monitor are called monitorable and non-monitorable, respectively. In this paper, we revise the notion of monitorability from a practical perspective, where we show how non-monitorable properties can still be used to generate partial monitors, which can partially check the properties. Finally, we present the implications both from a theoretical and practical perspectives.