Semantics and Algorithms for Parametric Monitoring

From FSL
Jump to: navigation, search

The work here has been published in a journal (J. LMCS) and previously in a conference (TACAS'09) and in a technical report. Note that the title of the journal paper is different from that of the conference, to better capture the foundational nature of this work.

J.LMCS

Semantics and Algorithms for Parametric Monitoring
Grigore Rosu and Feng Chen
J.LMCS, Volume 8(1), pp 1-47. 2012
Abstract. Analysis of execution traces plays a fundamental role in many program analysis approaches, such as runtime verification, testing, monitoring, and specification mining. Execution traces are frequently parametric, i.e., they contain events with parameter bindings. Each parametric trace usually consists of many meaningful trace slices merged together, each slice corresponding to one parameter binding. This gives a semantics-based solution to parametric trace analysis. A general-purpose parametric trace slicing technique is introduced, which takes each event in the parametric trace and dispatches it to its corresponding trace slices. This parametric trace slicing technique can be used in combination with any conventional, non-parametric trace analysis technique, by applying the later on each trace slice. As an instance, a parametric property monitoring technique is then presented. The presented parametric trace slicing and monitoring techniques have been implemented and extensively evaluated. Measurements of runtime overhead confirm that the generality of the discussed techniques does not come at a performance expense when compared with existing parametric trace monitoring systems.
PDF, MOP, DOI, J.LMCS, BIB



TACAS'09

Parametric Trace Slicing and Monitoring
Feng Chen and Grigore Rosu
TACAS'09, LNCS 5505, pp 246-261. 2009.
Abstract. Analysis of execution traces plays a fundamental role in many program analysis approaches. Execution traces are frequently parametric, i.e., containing events with parameter bindings, and therefore comprised of many meaningful trace slices merged together, each slice corresponding to a parameter binding. Several techniques have been proposed to analyze parametric traces, but they have limitations: some in the specification formalism, others in the type of traces they support; moreover, they share common notions, intuitions, even techniques and algorithms, suggesting that a fundamental understanding of parametric trace analysis is needed. This foundational paper gives the first solution to parametric trace analysis that is unrestricted by the type of parametric properties or traces that can be analyzed. First, a general purpose parametric trace slicing technique is discussed, which takes each event in the parametric trace and distributes it to its corresponding trace slices. This parametric trace slicing technique can be used in combination with any conventional, non-parametric trace analysis, by applying the later on each trace slice. An online monitoring technique is then presented based on the slicing technique, providing a logic-independent solution to runtime verification of parametric properties. The presented monitoring technique has been implemented and extensively evaluated. The results confirm that the generality of the discussed techniques does not come at a performance expense when compared with existing monitoring systems.
PDF, Slides (PPT), LNCS, TACAS'09, DBLP, BIB


Technical Report

Parametric Trace Slicing and Monitoring
Grigore Rosu and Feng Chen
Technical report UIUCDCS-R-2008-2977, July 2008
Abstract. Trace analysis plays a fundamental role in many program analysis approaches, such as runtime verification, testing, monitoring, and specification mining. Recent research efforts bring empirical evidence that execution traces are frequently comprised of many meaningful trace slices merged together, each slice corresponding to instances of relevant parameters. Several current trace analysis techniques and systems allow the specification of parametric properties, and the analysis of execution traces with respect to each instance of the parameters. However, the current solutions have limitations: some in the specification formalism, others in the type of trace they support; moreover, they share common notions, intuitions, even techniques and algorithms, suggesting that a fundamental study and understanding of parametric trace analysis is needed.
This foundational paper gives the first solution to parametric trace analysis that is unrestricted by the type of parametric property or trace that can be analyzed. First, a general purpose parametric trace slicing technique is discussed, which takes each event in the parametric trace and distributes it to its corresponding trace slices. This parametric trace slicing technique can be used in combination with any conventional, non-parametric trace analysis technique, by applying the later on each trace slice. As an instance, a parametric property monitoring technique is then presented, which processes each trace slice online. Thanks to the generality of parametric trace slicing, the parametric property monitoring technique reduces to encapsulating and indexing unrestricted and well-understood non-parametric property monitors (e.g., finite or push-down automata).
The presented parametric trace slicing and monitoring techniques have been implemented and extensively evaluated. Measurements of runtime overhead confirm that the generality of the discussed techniques does not come at a performance expense when compared with existing parametric trace monitoring systems.
PDF, TR@UIUC, BIB

Personal tools
Namespaces

Variants
Actions
Navigation