Formal Specification of OWL-S with Object-Z

Semantic Web Services, one of the most significant research a reas within the Semantic Web vision, has been recognized as a promising technol- ogy that exhibits huge commercial potential, and attracts a great deal of attention from both the research community and Industry. OWL-S, one of the most sig- nificant Semantic Web Service ontologies proposed to date, p rovides Web Ser- vice providers with a core ontological framework and guidelines for describing the properties and capabilities of their Web Services in unambiguous, computer- intepretable form. To support standardization and tool support of OWL-S, a for- mal semantics of the language is highly desirable. In this paper, we present a for- mal Object-Z semantics of OWL-S. Different aspects of the language have been precisely defined within one unified framework. This model no t only provides a formal unambiguous model which can be used to develop tools and facilitate future development, but as demonstrated in the paper, can be used to identify and eliminate errors in the current documentation.