DejaVu: A Monitoring Tool for First-Order Temporal Logic

Abstract

Runtime Verification (rv) is aimed at analyzing individual execution traces and temporal behaviors observed from running programs and systems. Its traditional purpose is in detecting the lack of conformance with respect to a formal specification. While very early rv systems were based on specifications given in some form of propositional temporal logic, recent efforts have focused on monitoring so-called parametric specifications over events that carry data. Since a monitor for such specifications has to store observed data, the challenge is to have an efficient representation and manipulation of data. The fundamental problem is that the actual values of the data are not necessarily bounded or provided in advance. In this paper, we describe our monitoring tool, DejaVu, which implements our algorithm [HPU17] for monitoring first-order past linear-time temporal logic over a sequence of events that carry data. We propose the use of Binary Decision Diagrams (bdds) [Bry86] for representing and manipulating sets of observed data since (1) bdds provide highly compact representations, (2) operations over bdds, in particular complementation, are very efficient, and (3) the monitor construction for the propositional case shown in [HR02] naturally extends to bdds. Our experiments show a substantial improvement in performance compared to a related tool.