Skip to main content
Skip main navigation
No Access

Verification for commitment-based web service protocols

Published Online:pp 217-223https://doi.org/10.1504/IJWMC.2014.062006

We propose a model for a class of web services which are powered by relational databases and annotated by social commitment. Our model can be viewed as an extension of WSDL specification where schemas of service operations specify not only input-output signatures but also data constraints, control-flow constraints, state/output/effect rules. The data-aware temporal properties about interactions between services and users are specified in Linear Temporal First-Order Logic with Social Commitment (LTL-FOSC). We have proved it is possible to use existing tools (e.g. WAVE) originally designed for verification of web applications to verify such properties.

Keywords

web service, automatic verification, linear temporal logic

References

  • 1. Abiteboul, S. , Vianu, V. , Fordham, B. , Yesha, Y. (1998). ‘Relational transducers for electronic commerce’. Proceedings of the 17th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS’98). New York, NY, USA, ACM, 179-187 Google Scholar
  • 2. Berardi, D. , Calvanese, D. , De Giacomo, G. , Mecella, M. (2005). ‘Composition of services with nondeterministic observable behavior’. Service-Oriented Computing-ICSOC 2005, 520-526 Google Scholar
  • 3. Chinnici, R. , Moreau, J-J. , Ryman, A. , Weerawarana, S. (2007). ‘Web services description language (WSDL) version 2.0 part 1: Core language’. W3C Recommendation. 26, Google Scholar
  • 4. Damaggio, E. , Deutsch, A. , Hull, R. , Vianu, V. (2011). ‘Automatic verification of data-centric business processes’. Business Process Management. 3-16 Google Scholar
  • 5. Deutsch, A. , Marcus, M. , Sui, L. , Vianu, V. , Zhou, D. (2005). ‘A verifier for interactive, data-driven web applications’. Proceedings of the 2005 ACM SIGMOD International Conference on Management of Data. ACM, 539-550 Google Scholar
  • 6. Deutsch, A. , Sui, L. , Vianu, V. (2007). ‘Specification and verification of data-driven web applications’. Journal of Computer and System Sciences. 73, 3, 442-474 Google Scholar
  • 7. Emerson, E.A. (1990). ‘Temporal and modal logic’. Handbook of Theoretical Computer Science. 2, 995-1072 Google Scholar
  • 8. Fornara, N. , Viganò, F. , Verdicchio, M. , Colombetti, M. (2008). ‘Artificial institutions: a model of institutional reality for open multiagent systems’. Artificial Intelligence and Law. 16, 1, 89-105 Google Scholar
  • 9. Grønbæk, F. (2003). Web Services and Service Oriented Architecture. Workshop Google Scholar
  • 10. Lapadula, A. , Pugliese, R. , Tiezzi, F. (2007). ‘A calculus for orchestration of web services’. Programming Languages and Systems. 33-47 Google Scholar
  • 11. Mallya, A.U. , Singh, M.P. (2005). ‘Modeling exceptions via commitment protocols’. Proceedings of the 4th International Joint Conference on Autonomous Agents and Multiagent Systems. 122-129 Google Scholar
  • 12. Martin, D. , Burstein, M. , Mcdermott, D. , Mcilraith, S. , Paolucci, M. , Sycara, K. , Mcguinness, D.L. , Sirin, E. , Srinivasan, N. (2007). ‘Bringing semantics to web services with OWL-S’. World Wide Web. 10, 3, 243-277 Google Scholar
  • 13. Singh, M.P. (2000). ‘A social semantics for agent communication languages’. Issues in Agent Communication. Springer, 31-45 Google Scholar
  • 14. Spielmann, M. (2003a). ‘Automatic verification of abstract state machines’. Proceedings of the 11th International Conference on Computer Aided Verification. 40-65 Google Scholar
  • 15. Spielmann, M. (2003b). ‘Verification of relational transducers for electronic commerce’. Journal of Computer and System Sciences. 66, 1, 40-65 Google Scholar
  • 16. Telang, P.R. , Singh, M.P. (2009). ‘Business modeling via commitments’. Service-Oriented Computing: Agents, Semantics, and Engineering. Springer, 111-125 Google Scholar