Automatic Verification of Data-centric Web Service Specifications

Amodel are proposed for modeling data-centric Web services which are powered by relational databases and interact with users according to logical formulas specifying input constraints, control-flow constraints and state/output/action rules. The Linear Temporal First-Order Logic (LTL-FO) formulas over inputs, states, outputs and actions are used to express the properties to be verified.We have proven that automatic verification of LTL-FO properties of data-centric Web services under input-bounded constraints is decidable by reducing Web services to data-centric Web applications. Thus, we can verify Web service specifications using existing verifier designed for Web applications.