Formal Semantics of OWL-S with Rewrite Logic

Ning Huang, Xiaojuan Wang, Camilo Rocha

Beihang University, Beijing, China.
University of Illinois at Champaign Urbana, USA.

DOI: 10.4236/jsea.2009.21004                

Abstract

SOA is built upon and evolving from older concepts of distributed computing and modular programming, OWL-S plays a key role in describing behaviors of web services, which are the essential of the SOA software. Although OWL-S has given semantics to concepts by ontology technology, it gives no semantics to control-flow and data-flow. This paper presents a formal semantics framework for OWL-S sub-set, including its abstraction, syntax, static and dynamic seman-tics by rewrite logic. Details of a consistent transformation from OWL-S SOS of control-flow to corresponding rules and equations, and dataflow semantics including “Precondition”, “Result” and “Binding” etc. are explained. This paper provides a possibility for formal verification and reliability evaluation of software based on SOA.

Keywords

SOA, Web Services, OWL-S, Formal Semantics, Rewrite Logic, Consistent Transformation, Reliability Evaluation

Conflicts of Interest

The authors declare no conflicts of interest.

References

[1]	X. Fu, T. Bultan, and J. W. Su, “Analysis of interacting bpel web services,” in Proceedings of the 13th Interna-tional Conference on World Wide Web, New York, NY,USA, pp. 621-630, May 2004.
[2]	D. Martin, M. Burstein, J. Hobbs, O. Lassila, D. McDer-mott, S. McIlraith, S. Narayanan, M. Paolucci, B. Parsia, T. R. Payne, E. Sirin, N. Srinivasan, and K. Sycara, “OWL-S: Semantic markup for web services,” Technical Report UNSPECIFIED, Member Submission, W3C, http://www.w3.org/Submission/ OWL-S/, 2004.
[3]	H. Huang, W. T. Tsai, R. Paul, and Y. N. Chen, “Auto-mated model checking and testing for composite web ser- vices,” in Proceedings Eighth IEEE International Sympo sium on Object-Oriented Real-Time Distributed Computing, Washington, DC, USA, pp. 300-307, May 2005.
[4]	S. Narayanan and S. A. Mcllraith, “Simulation, verifi-cation and automated composition of web services,” in Proceedings 11th International Conference on World Wide Web, Honolulu, Hawaii, USA, pp. 77-88, May 2002.
[5]	A. Ankolekar, M. Paolucci, and K. Sycara, “Spinning the OWL-S process model-toward the verification of the OWL-S process models,” in Proceedings International Semantic Web Conference 2004 Workshop on Semantic Web Services: Preparing to Meet the World of Business Applications, Hiroshima, Japan, 2004.
[6]	H. H. Wang, A. Saleh, T. Payne, and N. Gibbins, “Formal specification of OWL-S with Object-Z: The static aspect,” in Proceedings IEEE/WIC/ACM International Conference on Web Intelligence, Washington, DC, USA, pp. 431-434, November 2007.
[7]	J. S. Dong, C. H. Lee, Y. F. Li, and H. Wang, “Verifying DAML+OIL and beyond in Z/EVES,” in Proceedings the 26th International Conference on Software Engineering, Washington, DC, USA, pp. 201-210, May 2004.
[8]	T. F. Serbanuta, F. Rosu, and J. Meseguer, “A rewriting logic approach to operational semantics (Extended Ab-stract),” Electronic Notes Theoretical Computer Science, Vol. 192, No. 1, pp. 125-141, October 2007.
[9]	H. Huang and R. A. Mason, “Model checking technolo-gies for web services,” in Proceedings the 4th IEEE Workshop on Software Technologies for Future Embed-ded and Ubiquitous Systems, and the Second International Workshop on Collaborative Computing, Integration, and Assurance, Wanshington, DC, USA, pp. 217-224, April 2006.
[10]	A. Verdejo and N. Marti-Oliet, “Executable structural operational semantics in maude,” Journal of Logic and Algebraic Programming, Vol. 67, No. 1-No. 2, pp. 226-293, April-May 2006.
[11]	M. Birna van Riemsdijk, Frank S. de Boer, M. Dastani, and John-Jules Meyer, “Prototyping 3APL in the maude term rewriting language,” in Proceedings of the fifth in-ternational joint conference on Autonomous agents and multiagent systems, Hakodate, Hokkaido, Japan, pp. 1279-1281, May 2006.
[12]	M. Clavel, F. Duran, S. Eker, P. Lincoln, N. M. Oliet, J. Meseguer, and C. Talcott, “All about maude-A high-per-formance logical framework,” Springer-Verlag New York, Inc., 2007.
[13]	J. Meseguer and G. Rou, “The rewriting logic semantics project,” Theoretical Computer Science, Vol. 373, No. 3, pp. 213-237, April 2007.
[14]	M. Clavel, F. Duran, etc., “Maude mannual,” Department of Computer Science University of Illinois at Urbana- Champaign, 2007, http://maude.cs.uiuc.edu