TP-DejaVu: Combining Operational and Declarative Runtime Verification

Runtime verification (RV) facilitates monitoring the executions of a system, comparing them against a formal specification. A main challenge is to keep the incremental complexity of updating its internal structure, each time a new event is inspected, to a minimum. There is a tradeoff between achieving a low incremental complexity and the expressive power of the used specification formalism. We present an efficient RV tool that allows specifying properties of executions that include data, with the possibility to apply arithmetic operations and comparisons on the data values. In order to be able to apply efficient RV for specifications with these capabilities, we combine two RV methodologies: the first one is capable of performing arithmetic operations and comparisons based on the most recent events; the second is capable of handling many events with data and relating events that occur at arbitrary distance in the observed execution. This is done by two phase RV, where the first phase, which monitors the input events directly and is responsible to the arithmetic calculations and comparisons, feeds the second phase with modified events for further processing. This is implemented as a tool called TP-DejaVu, which extends the DejaVu tool.