Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Lomuscio, A., Qu, H., Solanki, M.: Towards verifying compliance in agent-based web service compositions. In: Proceedings of The Seventh International Joint Conference on Autonomous Agents and Multi-agent systems (AAMAS 2008). ACM Press, New York (2008)
Ankolekar, A., Paolucci, M., Sycara, K.P.: Towards a formal verification of owl-s process models. In: Gil, Y., Motta, E., Benjamins, V.R., Musen, M.A. (eds.) ISWC 2005. LNCS, vol. 3729, pp. 37–51. Springer, Heidelberg (2005)
Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: A new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
CMU: An API for OWL-S. CMU OWL-S API, http://www.daml.ri.cmu.edu/owlsapi/index.html
Booth, D., Haas, H., McCabe, F., Newcomer, E., Champion, M., Ferris, C., Orchard, D.: Web service architecture. W3c working group note (February 11, 2004), http://www.w3.org/TR/ws-arch/
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge (1995)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)
Holzmann, G.J.: SPIN Model Checker, The: Primer and Reference Manual. Addison Wesley Professional, Reading (2003)
Huang, H., Tsai, W., Paul, R., Chen, Y.: Automated model checking and testing for composite web services. In: Proc. of ISORC 2005, pp. 300–307. IEEE Computer Society, Los Alamitos (2005)
Kalyanpur, A., Jimnez, D.: Automatic mapping of owl ontologies into java. In: Proceedings of Software Engeering and Knowledge Engeering (SEKE 2004) (2004)
Lomuscio, A., Qu, H., Raimondi, F.: Mcmas 0.9 alpha (2008), http://sourceforge.net/projects/ist-contract/
Lomuscio, A., Raimondi, F.: MCMAS: A model checker for multi-agent systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 450–454. Springer, Heidelberg (2006)
Lomuscio, A., Qu, H., Sergot, M.J., Solanki, M.: Verifying temporal and epistemic properties of web service compositions. In: Krämer, B.J., Lin, K.-J., Narasimhan, P. (eds.) ICSOC 2007. LNCS, vol. 4749, pp. 456–461. Springer, Heidelberg (2007)
Kavantzas, N., Burdett, D., Ritzinger, G., Fletcher, T., Lafon, Y.: Web Services Choreography Description Language Version 1.0: W3C Working Draft (December 17, 2004)
OASIS Web service Business Process Execution Language (WSBPEL) TC. Web service Business Process Execution Language Version 2.0 (2007)
The OWL-S Coalition. OWL-S 1.1 Release (2004), http://www.daml.org/services/owl-s/1.0/
Traverso, P., Pistore, M.: Automated composition of semantic web services into executable processes. In: McIlraith, S.A., Plexousakis, D., van Harmelen, F. (eds.) ISWC 2004. LNCS, vol. 3298, pp. 380–394. Springer, Heidelberg (2004)
Wooldridge, M.: An introduction to multi-agent systems. John Wiley, England (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lomuscio, A., Solanki, M. (2009). Towards an Agent Based Approach for Verification of OWL-S Process Models. In: Aroyo, L., et al. The Semantic Web: Research and Applications. ESWC 2009. Lecture Notes in Computer Science, vol 5554. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02121-3_43
Download citation
DOI: https://doi.org/10.1007/978-3-642-02121-3_43
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02120-6
Online ISBN: 978-3-642-02121-3
eBook Packages: Computer ScienceComputer Science (R0)