Automatic Verification of Data-Driven Web Services
Victor Vianu ( USCD )
The talk describes models of Web services and their compositions, and results on their automatic verification.
After a brief review of finite-state models of Web services, the talk focuses on infinite-state models and
verification results taking into account the presence of data. Web services accessing an underlying database
are modeled as transducers whose control is specified in first-order logic.
Compositions of Web services are modeled by communicating transducers. The properties to be verified
are expressed in an extended LTL where propositions are interpreted as FO formulas. The results establish
under what conditions automatic verification of such properties is possible and provide the complexity of verification.
This relies on a novel coupling of database and model checking techniques. A verifier relying on these techniques
has also been implemented, with surprisingly good verification times. The theoretical and practical results
suggest that automatic verification of a significant class of data-driven applications may well be within reach.
Joint work with Alin Deutsch, Liying Sui and Dayou Zhou (UC San Diego)