From First-order Temporal Logic to Parametric Trace Slicing

Abstract. Parametric runtime verification is the process of verifying properties of execution traces of (data carrying) events produced by a running system. This paper considers the relationship between two widely-used specification approaches to parametric runtime verification: trace slicing and first-order temporal logic. This work is a first step in understanding this relationship. We introduce a technique of identifying syntactic fragments of temporal logics that admit notions of sliceability. We show how to translate formulas in such fragments into automata with a slicing-based semantics. In exploring this relationship, the paper aims to allow monitoring techniques to be shared between the two approaches and initiate a wider effort to unify specification languages for runtime verification.

• Type: Journal
• Year: 2015
• Where: RV
• Authors: Giles Reger, David E. Rydeheard
• Keywords: Hardware, RV 2015