A Story of Parametric Trace Slicing, Garbage and Static Analysis
This is an incremental improvement for runtime verification in Java, addressing specific bottlenecks in monitoring algorithms.
The paper tackles the problem of improving runtime verification for Java by statically detecting unreachable objects to enhance parametric trace slicing, proposing to integrate these techniques into the MarQ monitoring tool.
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.