Formal Reasoning on a Web Coordination System

  • Eloy J. Mata
  • Pedro Álvarez
  • José A. Bañares
  • Julio Rubio
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4739)


In this paper, a first step toward the use of Artificial Intelligence tools (namely proof assistants) in the formal analysis of programs for Web services coordination is presented. This first attempt consists in the formal modeling of a system with transactional capabilities. The model is devised on a variant of the well-known Linda model for generative communication. We explore then the role of the Rete algorithm to implement efficiently a transactional read operation, opening the way for a further formal analysis of it, by means of automated testing against a certified program (i.e. a program verified with the help of a proof assistant).


Formal Reasoning Coordination Model Proof Assistant Tuple Space Java Object 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Andrés, M., Lambán, L., Rubio, J.: Executing in Common Lisp, Proving in ACL2. In: Calculemus 2007. LNCS, vol. 4573, pp. 1–12. Springer, Heidelberg (2007)Google Scholar
  2. 2.
    Gelernter, D.: Generative communication in Linda. ACM Transactions on Programming Languages and Systems 7(1), 80–112 (1985)zbMATHCrossRefGoogle Scholar
  3. 3.
    Viroli, M., Ricci, A.: Tuple-Based Coordination Models in Event-Based Scenarios. In: IEEE 22nd International Conference on Distributed Computing Systems (ICDCS 2002 Workshops) - DEBS 2002 International Workshop on Distributed Event-Based Systems, Vienna, Austria (July 2002)Google Scholar
  4. 4.
    Mata, E., Álvarez, P., Bañares, J.A., Rubio, J.: Towards and Efficient Rule-Based Coordination of Web Services. In: Lemaître, C., Reyes, C.A., González, J.A. (eds.) IBERAMIA 2004. LNCS (LNAI), vol. 3315, pp. 73–82. Springer, Heidelberg (2004)Google Scholar
  5. 5.
    Mata, E., Álvarez, P., Bañares, J.A., Rubio, J.: Formal Modelling of a Coordination System: from Practice to Theory and back again. In: Mata, E., Álvarez, P. (eds.) Engineering Societies in the Agents World VII, ESAW 2006, Dublin, Ireland. LNCS (LNAI), Springer, Heidelberg (2007)Google Scholar
  6. 6.
    Forgy, C.: A fast algorithm for many pattern / many object pattern match problem. Artificial Intelligence 19, 17–37 (1982)CrossRefGoogle Scholar
  7. 7.
    Doorenbos, R.B.: Production Matching for Large Learning Systems (Rete/UL). PhD thesis, Carnegie Mellon University (1995)Google Scholar
  8. 8.
    Álvarez, P., Bañares, J.A., Muro-Medrano, P.: An Architectural Pattern to Extend the Interaction Model between Web-Services: The Location-Based Service Context. In: Orlowska, M.E., Weerawarana, S., Papazoglou, M.M.P., Yang, J. (eds.) ICSOC 2003. LNCS, vol. 2910, pp. 271–286. Springer, Heidelberg (2003)Google Scholar
  9. 9.
    Busi, N., Ciancarini, P., Gorrieri, R., Zavattaro, G.: Coordination Models: A Guided Tour. In: Coordination of Internet Agents, pp. 6–24. Springer, Heidelberg (2001)Google Scholar
  10. 10.
    Rowstron, A., Wood, A.: Solving the Linda multiple rd problem using the copy-collect primitive. Science of Computer Programming 31(2-3), 335–358 (1998)zbMATHCrossRefGoogle Scholar
  11. 11.
    Zavattaro, G.: Coordination Models and Languages: Semantics and expressiveness. PhD thesis, Department of Computer Science, University of Bologna, Italy (2000)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Eloy J. Mata
    • 1
  • Pedro Álvarez
    • 2
  • José A. Bañares
    • 2
  • Julio Rubio
    • 1
  1. 1.Departamento de Matemáticas y Computación, Universidad de La Rioja, Edificio Vives, Luis de Ulloa s/n, E-26004 Logroño (La Rioja, Spain) 
  2. 2.Departamento de Informática e Ingeniería de Sistemas, Universidad de Zaragoza, María de Luna 3, E-50015 ZaragozaSpain

Personalised recommendations