RV'04 Preliminary Version Monitoring Algorithms for Metric Temporal Logic Specifications

1 Introduction Runtime verification and monitoring have been proposed as lightweight formal verification methods [13] with the explicit goal of checking systems against their formal requirements while they execute. In most monitoring applications, execution traces are available only incrementally and they are much larger than the formulae against which they are checked. Storing an entire execution trace and then performing the formal analysis by having random access to the trace is very expensive and sometimes even impossible. For example, the monitor may lack resources, e.g., if it runs within an embedded system, or the monitor may be expected to react promptly when its requirements are violated, in order for the system to safely take a recovery or a shutdown action. In this paper, we adopt the position that a monitoring algorithm does not store execution traces, but rather consumes the events as they are received from the monitored program. The problem of checking execution trace