Automatic Verification of Data-Driven Web Services

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)