A Story of Parametric Trace Slicing, Garbage and Static Analysis

TL;DR

This paper explores how static analysis for unreachable objects in Java can enhance parametric trace slicing in runtime verification, aiming to improve garbage management and property violation detection.

Contribution

It proposes making object unreachability explicit in parametric properties and adding instrumentation points, integrating static analysis with runtime monitoring techniques.

Findings

Conceptual framework for static-unreachability integration

Potential improvements in garbage collection handling

Enhanced detection of property violations

Abstract

This paper presents a proposal (story) of how statically detecting unreachable objects (in Java) could be used to improve a particular runtime verification approach (for Java), namely parametric trace slicing. Monitoring algorithms for parametric trace slicing depend on garbage collection to (i) cleanup data-structures storing monitored objects, ensuring they do not become unmanageably large, and (ii) anticipate the violation of (non-safety) properties that cannot be satisfied as a monitored object can no longer appear later in the trace. The proposal is that both usages can be improved by making the unreachability of monitored objects explicit in the parametric property and statically introducing additional instrumentation points generating related events. The ideas presented in this paper are still exploratory and the intention is to integrate the described techniques into the MarQ monitoring tool for quantified event automata.