Runtime Monitoring of Message-Based Workflows with Data

We present an algorithm for the runtime monitoring of business process properties with data parameterization. The properties are expressed in LTL-FO+, an extension to traditional Linear Temporal Logic that includes full first-order quantification over the data inside a trace of XML messages. The algorithm works "on-the-fly": it keeps in memory only the states that are necessary at each step. Initial results indicate that LTL-FO+ is an appropriate language for expressing data dependencies on message traces and that its processing overhead on sample traces is acceptable.