Checking Correctness of Transactional Behaviors

  • Vincenzo Ciancia
  • Gian Luigi Ferrari
  • Roberto Guanciale
  • Daniele Strollo
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5048)


The Signal Calculus is an asynchronous process calculus featuring multicast communication. It relies on explicit modeling of the communication structure of the network (communication flows), and on handling sessions, even multi-party. The calculus is strongly motivated by the practical needs of Service-Oriented Computing, and there exists a Java implementation, called JSCL, with a graphical modeling framework. To the aim of adding to SC (and JSCL) a verification environment, in this work we introduce the abstract semantics of SC, based on bisimulation. We show an example exploiting bisimilarity to prove the correctness of an SC model with respects to a transactional isolation requirement.


Service Oriented Architectures Event Notification Coordination Observational Equivalence 


  1. 1.
    Aiello, M., Aoyama, M., Curbera, F., Papazoglou, M.P. (eds.): Service-Oriented Computing - ICSOC 2004, Second International Conference, Proceedings, November 15-19, 2004. ACM, New York (2004)Google Scholar
  2. 2.
    Amadio, R.M., Castellani, I., Sangiorgi, D.: On bisimulations for the asynchronous pi-calculus. Theor. Comput. Sci. 195(2), 291–324 (1998)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Bartoletti, M., Degano, P., Ferrari, G., Zunino, R.: Secure service orchestration. In: Hertzberg, J., Beetz, M., Englert, R. (eds.) KI 2007. LNCS (LNAI), vol. 4667. Springer, Heidelberg (2007)Google Scholar
  4. 4.
    Boreale, M., Bruni, R., Caires, L., De Nicola, R., Lanese, I., Loreti, M., Martins, F., Montanari, U., Ravara, A., Sangiorgi, D., Vasconcelos, V.T., Zavattaro, G.: Scc: A service centered calculus. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 38–57. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  5. 5.
    Carbone, M., Honda, K., Yoshida, N.: Structured communication-centred programming for web services. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 2–17. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  6. 6.
    Ciancia, V., Ferrari, G.L.: Co-Algebraic Models for Quantitative Spatial Logics. In: Quantitative Aspects of Programming Languages (QAPL 2007) (2007)Google Scholar
  7. 7.
    Ciancia, V., Montanari, U.: A name abstraction functor for named sets. Coalgebraic Methods in Computer Science (to appear, 2008)Google Scholar
  8. 8.
    Ferrari, G.L., Guanciale, R., Strollo, D.: Event based service coordination over dynamic and heterogeneous networks. In: Dan, A., Lamersdorf, W. (eds.) ICSOC 2006. LNCS, vol. 4294, pp. 453–458. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  9. 9.
    Ferrari, G.L., Montanari, U., Tuosto, E.: Coalgebraic minimization of hd-automata for the pi-calculus using polymorphic types. Theor. Comput. Sci. 331(2-3), 325–365 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Ferrari, G., Guanciale, R., Strollo, D.: Jscl: A middleware for service coordination. In: Najm, et al. [21], pp. 46–60.Google Scholar
  11. 11.
    Ferrari, G., Guanciale, R., Strollo, D.: An Eclipse plugin for designing and developing Web Service orchestrations in JSCL. Technical report (2007)Google Scholar
  12. 12.
    Ferrari, G., Guanciale, R., Strollo, D., Tuosto, E.: Coordination via types in an event-based framework. In: Derrick, J., Vain, J. (eds.) FORTE 2007. LNCS, vol. 4574, pp. 66–80. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  13. 13.
    Object Management Group. Business process modelling notation. Technical report,
  14. 14.
    Guidi, C., Lucchi, R., Gorrieri, R., Busi, N., Zavattaro, G.: A calculus for service oriented computing. In: Dan, A., Lamersdorf, W. (eds.) ICSOC 2006. LNCS, vol. 4294, pp. 327–338. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  15. 15.
    Honda, K., Tokoro, M.: An object calculus for asynchronous communication. In: America, P. (ed.) ECOOP 1991. LNCS, vol. 512, pp. 133–147. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  16. 16.
    IBM. Business Process Execution Language (BPEL). Technical report (2005)Google Scholar
  17. 17.
    Lapadula, A., Pugliese, R., Tiezzi, F.: A calculus for orchestration of web services. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 33–47. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  18. 18.
    Liu, Y., Plale, B.: Survey of publish subscribe event systems. Technical Report 574, Department of Computer Science, Indiana UniversityGoogle Scholar
  19. 19.
    Misra, J.: A programming model for the orchestration of web services. In: SEFM, pp. 2–11. IEEE Computer Society, Los Alamitos (2004)Google Scholar
  20. 20.
    Montanari, U., Pistore, M.: History Dependent Automata. Technical report, Dipartimento di Informatica, Università di Pisa, TR-11-98 (1998)Google Scholar
  21. 21.
    Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.): FORTE 2006. LNCS, vol. 4229. Springer, Heidelberg (2006)zbMATHGoogle Scholar
  22. 22.
    OMG. Business Process Modeling Language (2002),
  23. 23.
    W3C. Web Services Choreography Description Language (v.1.0). Technical reportGoogle Scholar
  24. 24.
    Wirsing, M., Clark, A., Gilmore, S., Hölzl, M.M., Knapp, A., Koch, N., Schroeder, A.: Semantic-based development of service-oriented systems. In Najm, et al [21], pp. 24–45Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2008

Authors and Affiliations

  • Vincenzo Ciancia
    • 1
  • Gian Luigi Ferrari
    • 1
  • Roberto Guanciale
    • 2
  • Daniele Strollo
    • 1
    • 2
  1. 1.Dipartimento di InformaticaUniversità degli Studi di PisaPisaItaly
  2. 2.Institute for Advanced Studies IMT LuccaLuccaItaly

Personalised recommendations