A Rewriting Logic Approach to OWL-S Composite Process Formal Specification

OWL-S is one of the leading standards for the description of Web services on the Semantic Web. However its composite process specification is lack of precise mathematic semantic which leads the process specification described in OWL-S is only a semi-formal one, and canpsilat do reasoning and formal analysis in this part. This paper proposes a formal framework for enriching composite process description with rewriting logic that facilitates compositional reasoning about services in OWL-S composite process model. The technique is based on Maude language, a rewriting logic based methodology in which formal modeling and analysis can be used from the earliest phases of system design to uncover many errors and inconsistencies in composition, and to reach high assurance for critical components with runtime verification of OWL-S composite process specification.