Presented at: 6th Annual European Semantic Web Conference (ESWC2009)
In this paper we investigate the transformation of OWL-S process models to ISPL - the system description language for MCMAS, a symbolic model checker for multi agent systems. We take the view that services can be considered as agents and service compositions as multi agent systems. We illustrate how atomic and composite processes in OWL-S can be encoded into ISPL using the proposed transformation rules for a restricted set of data types. As an illustrative example, we use an extended version of the BravoAir process model. We formalise certain interesting properties of the example in temporal-epistemic logic and present results from their verification using MCMAS.
Keywords: MCMAS, OWL-S, model checking, multi agent systems, verification, Semantic Web, Semantic Web Services, Test, Validation, Web service, Web Service
Resource URI on the dog food server: http://data.semanticweb.org/conference/eswc/2009/paper/88
Explore this resource elsewhere: