Complex Semantic Web (SW) services may have intricate data state, autonomous process behavior and concurrent interactions. The design of such SW service systems requires precise and powerful modelling techniques to capture not only the ontology domain properties but also the services' process behavior and functionalities. In this paper we apply an integrated formal modeling language, Timed Communicating Object Z (TCOZ), to design SW services. Furthermore, the paper presents the development of the systematic translation rules and tools which can automatically extract the SW ontology and services semantic markup from the formal TCOZ design model. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification-Formal methods; I.2.4 [Knowledge Representation Formalisms and Methods]: Representation languages Keywords Semantic Web, Formal Methods, TCOZ, DAML+OIL, DAML-S
Jin Song Dong, Yuan-Fang Li, Hai H. Wang