Home

Welcome to the DICE-Trace-Checking wiki!

DICE Trace checking tool (DICE-TraCT) is a component of D-mon platform which enables trace-checking for the applications developed through the DICE framework. Trace checking allows for the analysis of the runtime behavior of running applications that store the relevant execution events as sequences of timestamped events. The goal of the analysis is to establish whether the system logs - traces - satisfy a given property, usually specified in a logical language.

Trace checking is especially useful when the property used to assess logs cannot be inferred from the information collected by the monitoring system of the framework which executes the application. In some cases, in fact, the properties are related to specific non-functional application properties and do not depend on the physical infrastructure where the application runs.

Logical languages involved in the trace checking are usually extensions of metric temporal logics offering special operators called aggregating modalities. A formula containing such operators holds if the trace in analysis satisfies quantitative features like, for instance, a specific counting property of certain events occurring in the trace. DICE-TraCT uses Soloist [1] which allows the following class of aggregating modalities in the formulae:

• number of occurrences of an event e in a time window of length d,
• maximum/average number of occurrences of an event e, aggregated over right-aligned adjacent non-overlapping subintervals (of size h) in a time window of length d,
• average time elapsed between a pair of specific adjacent and alternating events e and e’ occurring in a time window of length d.

According to the DICE methodology, trace checking is performed after verification on a deployed application to allow for continuous model refinement. The result obtained with the log analysis might identify runtime issues representing undesired behavior of the application that must be eliminated through design refactory.

[1] Marcello M. Bersani, Domenico Bianculli, Carlo Ghezzi, Srdan Krstic, Pierluigi San Pietro: Efficient Large-scale Trace Checking Using MapReduce [pdf] (http://doi.acm.org/10.1145/2884781.2884832)