XML methods for validation of temporal properties on message traces with data

Abstract

We perform trace validation of LTL formulæ by exclusively using readily-available XML technologies. We first provide a translation between LTL and a subset of the XML Query Language XQuery, and show that an efficient validation of LTL formulæ can be achieved through the evaluation of XQuery expressions. Moreover, since LTL maps to a small fragment of XQuery, we show that that extending it to LTL-FO∈+∈, which includes full first-order quantification over message contents, can be supported without additional cost. All these capabilities, which come "for free" in any web service environment providing a standard XQuery engine, are tested using a representative choreography scenario. © 2008 Springer Berlin Heidelberg.