Semantics and algorithms for parametric monitoring

Analysis of execution traces plays a fundamental role in many program anal- ysis approaches, such as runtime verification, testing, monitoring, and specification min- ing. Execution traces are frequently parametric, i.e., they contain events with param- eter bindings. Each parametric trace usually consists of many meaningful trace slices merged together, each slice corresponding to one parameter binding. For example, a Java program creating iterator objects i₁ and i₂ over collection object c₁ may yield a trace createIter 〈c₁ i₁〉 next〈i₁〉 createIter〈c₁ i₂〉 updateColl〈c₁〉 next〈i₁〉 parametric in collection c and iterator i, whose slices corresponding to instances "c, i → c₁, i₁" and "c, i → c₁, i₂" are createIter〈c₁ i₁〉 next〈i₁〉 updateColl〈c₁〉 next〈i₁〉 and, respectively, createIter〈c₁ i₂〉 updateColl〈c₁〉. Several approaches have been proposed to specify and dynamically analyze parametric properties, but they have limitations: some in the specification formalism, others in the type of trace they support. Not unexpectedly, the existing approaches share common no- tions, intuitions, and even techniques and algorithms, suggesting that a fundamental study and understanding of parametric trace analysis is necessary. This foundational paper aims at giving a semantics-based solution to parametric trace analysis that is unrestricted by the type of parametric property or trace that can be analyzed. Our approach is based on a rigorous understanding of what a parametric trace/property/monitor is and how it relates to its non-parametric counter-part. 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, 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 imple- mented and extensively evaluated. Measurements of runtime overhead confirm that the generality of the discussed techniques does not come at a performance expense when com- pared with existing parametric trace monitoring systems.