| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 555445 | IERI Procedia | 2013 | 6 Pages |
Abstract
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Information Systems
