Towards verifying compliance in agent-based web service compositions

ABSTRACT

We explore the problem of specification and verification of compliance in agent based Web service compositions. We use the formalism of temporal-epistemic logic suitably extended to deal with compliance/violations of contracts. We illustrate these concepts using a motivating example where the behaviours of participating agents are governed by contracts. The composition is specified in OWL-S and mapped to our chosen formalism. Finally we use an existing symbolic model checker to verify the example specification whose state space is approximately 2²¹ and discuss experimental results.

REFERENCES

• 1: D. Booth, H. Haas, F. McCabe, E. Newcomer, M. Champion, C. Ferris, and D. Orchard. Web service architecture. w3c working group note 11 february 2004, 2004. http://www.w3.org/TR/ws-arch/.
• 2: R. Bordini, M. Fisher, C. Pardavila, W. Visser, and M. Wooldridge. Model checking multi-agent programs with CASP. In CAV'03, volume LNCS 2725, pages 110--113. Springer-Verlag, 2003.
• 3: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 4: Ronald Fagin , Joseph Y. Halpern , Moshe Y. Vardi , Yoram Moses, Reasoning about knowledge, MIT Press, Cambridge, MA, 1995
• 5: Xiang Fu , Tevfik Bultan , Jianwen Su, Analysis of interacting BPEL web services, Proceedings of the 13th international conference on World Wide Web, May 17-20, 2004, New York, NY, USA [doi>10.1145/988672.988756]
• 6: Hai Huang , Wei-Tek Tsai , Raymond Paul , Yinong Chen, Automated Model Checking and Testing for Composite Web Services, Proceedings of the Eighth IEEE International Symposium on Object-Oriented Real-Time Distributed Computing, p.300-307, May 18-20, 2005 [doi>10.1109/ISORC.2005.16]
• 7: A. Lomuscio and F. Raimondi. MCMAS: A model checker for multi-agent systems. In Proceedings of TACAS 2006, volume 3920, pages 450--454. Springer Verlag, 2006.
• 8: A. Lomuscio and M. Sergot. Deontic interpreted systems. Studia Logica, 75(1):63--92, 2003.
• 9: A. Lomuscio and M. Sergot. A formalisation of violation, error recovery, and enforcement in the bit transmission problem. Journal of Applied Logic, 2(1):93--116, Mar. 2004.
• 10: A. Lomuscio and B. Woźna. A complete and decidable axiomatisation for deontic interpreted systems. In Proceedings of the 8th International Workshop on Deontic Logic in Computer Science (DEON'06), volume 4048, pages 238--254. Springer-Verlag, July 2006.
• 11: Wojciech Penczek , Alessio Lomuscio, Verifying epistemic properties of multi-agent systems via bounded model checking, Fundamenta Informaticae, v.55 n.2, p.167-185, August 2002
• 12: M. Pistore, F. Barbon, P. Bertoli, D. Shaparau, and P. Traverso. Planning and monitoring web service composition. In AIMSA, pages 106--115, 2004.
• 13: The OWL-S Coalition. OWL-S 1.1 Release., 2004. http://www.daml.org/services/owl-s/1.0/.
• 14: Michael Woolridge , Michael J. Wooldridge, Introduction to Multiagent Systems, John Wiley & Sons, Inc., New York, NY, 2001
• 15: M. Wooldridge, M.-P. Huget, M. Fisher, and S. Parsons. Model checking for multiagent systems: the mable language and its applications. International Journal on Artificial Intelligence Tools, 15(2):195--226, 2006.
• 16: X. Fu T. Bultan and J. Su. Conversation Protocols: A Formalism for Specification and Verification of Reactive Electronic Services. In CIAA, volume LNCS 2759, pages 188--200. Springer-Verlag, 2003.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  H. Information Systems
  H.3 INFORMATION STORAGE AND RETRIEVAL
      H.3.5 On-line Information Services

General Terms:
Verification

Keywords:
compliance, epistemic logic, model checking, web services