Towards Partial Monitoring: It is Always too Soon to Give Up
Open Access
- 21 October 2021
- journal article
- Published by Open Publishing Association in Electronic Proceedings in Theoretical Computer Science
- Vol. 348, 38-53
- https://doi.org/10.4204/eptcs.348.3
Abstract
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.This publication has 27 references indexed in Scilit:
- Sliding between Model Checking and Runtime VerificationLecture Notes in Computer Science, 2013
- Runtime Verification for LTL and TLTLACM Transactions on Software Engineering and Methodology, 2011
- A brief account of runtime verificationThe Journal of Logic and Algebraic Programming, 2009
- Monitoring of Real-Time PropertiesLecture Notes in Computer Science, 2006
- Monitoring Temporal Properties of Continuous SignalsLecture Notes in Computer Science, 2004
- Computational Analysis of Run-time Monitoring: Fundamentals of Java-MaCElectronic Notes in Theoretical Computer Science, 2002
- Safety, liveness and fairness in temporal logicFormal Aspects of Computing, 1994
- Proof systems for satisfiability in Hennessy-Milner Logic with recursionTheoretical Computer Science, 1990
- Recognizing safety and livenessDistributed Computing, 1987
- Hierarchical verification of asynchronous circuits using temporal logicTheoretical Computer Science, 1985