A Story of Parametric Trace Slicing, Garbage and Static Analysis

Giles Reger
(University of Manchester, UK)

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.

In Adrian Francalanza and Gordon J. Pace: Proceedings Second International Workshop on Pre- and Post-Deployment Verification Techniques (PrePost 2017), Torino, Italy, 19 September 2017, Electronic Proceedings in Theoretical Computer Science 254, pp. 1–14.
Published: 23rd August 2017.

ArXived at: http://dx.doi.org/10.4204/EPTCS.254.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org