Specifying and Analysing SOC Applications with COWS

  • Alessandro Lapadula
  • Rosario Pugliese
  • Francesco Tiezzi
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5065)


COWS is a recently defined process calculus for specifying and combining service-oriented applications, while modelling their dynamic behaviour. Since its introduction, a number of methods and tools have been devised to analyse COWS specifications, like e.g. a type system to check confidentiality properties, a logic and a model checker to express and check functional properties of services. In this paper, by means of a case study in the area of automotive systems, we demonstrate that COWS, with some mild linguistic additions, can model all the phases of the life cycle of service-oriented applications, such as publication, discovery, negotiation, orchestration, deployment, reconfiguration and execution. We also provide a flavour of the properties that can be analysed by using the tools mentioned above.


Credit Card Service Level Agreement Service Discovery Service Description Estimate Travel Time 
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.
    CMS: an on-the-fly model checker and interpreter for COWS,
  2. 2.
    Software Engineering for Service-Oriented Overlay Computers (Sensoria) (2005),
  3. 3.
    ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: An action/state-based model-checking approach for the analysis of communication protocols for Service-Oriented Applications. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol. 4916, pp. 133–148. Springer, Heidelberg (2008)Google Scholar
  4. 4.
    Bistarelli, S., Montanari, U., Rossi, F.: Semiring-based constraint satisfaction and optimization. Journal of the ACM 44(2), 201–236 (1997)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Buscemi, M., Montanari, U.: CC-Pi: A Constraint-Based Language for Specifying Service Level Agreements. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 18–32. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  6. 6.
    De Nicola, R., Gorla, D., Pugliese, R.: Confining data and processes in global computing applications. Science of Computer Programming 63, 57–87 (2006)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    De Nicola, R., Vaandrager, F.: Three logics for branching bisimulation. J. ACM 42(2), 458–487 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    De Nicola, R., Vaandrager, F.W.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990)Google Scholar
  9. 9.
    Fantechi, A., Gnesi, S., Lapadula, A., Mazzanti, F., Pugliese, R., Tiezzi, F.: A model checking approach for verifying COWS specifications. In: Fiadeiro, J., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 230–245. Springer, Heidelberg (2008)Google Scholar
  10. 10.
    Fiadeiro, J., Lopes, A., Bocchi, L.: A formal approach to service component architecture. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 193–213. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  11. 11.
    Garcia-Molina, H., Salem, K.: Sagas. In: SIGMOD, pp. 249–259. ACM Press, New York (1987)Google Scholar
  12. 12.
    Kirli, Z.D.: Confined mobile functions. In: 14th IEEE Computer Security Foundations Workshop (CSFW 2001), pp. 283–294. IEEE Computer Society, Los Alamitos (2001)CrossRefGoogle Scholar
  13. 13.
    Koch, N.: Automotive case study: UML specification of on road assistance scenario. Technical Report 1, FAST (2007),
  14. 14.
    Lapadula, A., Pugliese, R., Tiezzi, F.: A Calculus for Orchestration of Web Services (full version). Technical report, Dipartimento di Sistemi e Informatica, Univ. Firenze (2006),
  15. 15.
    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
  16. 16.
    Lapadula, A., Pugliese, R., Tiezzi, F.: COWS specification of the on road assistance scenario. Technical report, Dipartimento di Sistemi e Informatica, Univ. Firenze (2007),
  17. 17.
    Lapadula, A., Pugliese, R., Tiezzi, F.: COpen image in new windowWS: A timed service-oriented calculus. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 275–290. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  18. 18.
    Lapadula, A., Pugliese, R., Tiezzi, F.: Regulating data exchange in service oriented applications. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol. 4767, pp. 223–239. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  19. 19.
    Lapadula, A., Pugliese, R., Tiezzi, F.: Service discovery and negotiation with COWS. In: WWV. ENTCS, Elsevier, Amsterdam (2007)Google Scholar
  20. 20.
    Meredith, L.G., Bjorg, S.: Contracts and types. Commun. ACM 46(10), 41–47 (2003)CrossRefGoogle Scholar
  21. 21.
    Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, I and II. Inf. Comput. 100(1), 1–40, 41–77 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  22. 22.
    OASIS WSBPEL TC. Web Services Business Process Execution Language Version 2.0. Technical report, OASIS, April (2007),
  23. 23.
    Prandi, D., Quaglia, P.: Stochastic COWS. In: Krämer, B.J., Lin, K.-J., Narasimhan, P. (eds.) ICSOC 2007. LNCS, vol. 4749, pp. 245–256. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  24. 24.
    van Breugel, F., Koshkina, M.: Models and verification of bpel. Technical report (2006),
  25. 25.
    van Glabbeek, R.J.: On specifying timeouts. ENTCS 162, 173–175 (2006)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Alessandro Lapadula
    • 1
  • Rosario Pugliese
    • 1
  • Francesco Tiezzi
    • 1
  1. 1.Dipartimento di Sistemi e InformaticaUniversità degli Studi di Firenze 

Personalised recommendations