A practical approach to runtime verification of real-time properties for Java programs

Given the intractability of exhaustively verifying soft-ware, the use of runtime-verification to verify single execution paths at runtime, is becoming increasingly popular in industrial settings. In this paper we present dynamic communicating automata with timers and events to describe properties of systems, implemented in LARVA, an event-based runtime verification tool for monitoring temporal and contextual properties of Java programs. We give the mathematical framework behind LARVAand show how real time logics can be trans-lated into LARVAproviding additional benefits to the runtime monitoring framework. These benefits include guarantees on the memory upperbound required for the monitoring system and guarantees on the effect of varying the execution speed of the system with regards to real-time properties. Index Terms runtime verification, real-time properties, duration cal-culus 1.peer-reviewe