JPL Technical Report Server

Efficient Runtime Verification of First-Order Temporal Properties

Show simple item record Havelund, Klaus Peled, Doron 2020-05-07T00:56:05Z 2020-05-07T00:56:05Z 2018-07-15
dc.identifier.citation FM 2018: 22nd International Symposium on Formal Methods, Oxford, United Kingdom, July 15 - 17, 2018 en_US
dc.identifier.clearanceno 18-2474
dc.description.abstract Runtime verification allows monitoring the execution of a system against a temporal property, raising an alarm if the property is violated. In this paper we present a theory and system for runtime verification of a first-order past time linear temporal logic. The first-order nature of the logic allows a monitor to reason about events with data elements. While runtime verification of propositional temporal logic requires only a fixed amount of memory, the first-order variant has to deal with a number of data values potentially growing unbounded in the length of the execution trace. This requires special compactness considerations in order to allow checking very long executions. In previous work we presented an efficient use of BDDs for such first-order runtime verification, implemented in the tool DEJAVU. We first summarize this previous work. Subsequently, we look at the new problem of dynamically identifying when data observed in the past are no longer needed, allowing to reclaim the data elements used to represent them. We also study the problem of adding relations over data values. Finally, we present parts of the implementation, including a new concept of user defined property macros. 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 Efficient Runtime Verification of First-Order Temporal Properties en_US
dc.type Preprint en_US

Files in this item

This item appears in the following Collection(s)

Show simple item record



My Account