JPL Technical Report Server

DejaVu: A Monitoring Tool for First-Order Temporal Logic

Show simple item record

dc.contributor.author Havelund, Klaus
dc.contributor.author Peled, Doron
dc.contributor.author Ulus, Dogan
dc.date.accessioned 2020-05-04T16:38:59Z
dc.date.available 2020-05-04T16:38:59Z
dc.date.issued 2018-04-10
dc.identifier.citation 3rd Workshop on Monitoring and Testing of Cyber-Physical Systems, Porto, Portugal, April 10, 2018 en_US
dc.identifier.clearanceno 18-2040
dc.identifier.uri http://hdl.handle.net/2014/48217
dc.description.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. en_US
dc.description.sponsorship NASA/JPL en_US
dc.language.iso en_US en_US
dc.publisher Pasadena, CA: Jet Propulsion Laboratory, National Aeronautics and Space Administration, 2018 en_US
dc.title DejaVu: A Monitoring Tool for First-Order Temporal Logic en_US
dc.type Preprint en_US


Files in this item

This item appears in the following Collection(s)

Show simple item record

Search


Browse

My Account