Playing with Our CAT and Communication-Centric Applications

  • Davide BasileEmail author
  • Pierpaolo Degano
  • Gian-Luigi Ferrari
  • Emilio Tuosto
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9688)


We describe CAT, a toolkit supporting the analysis of communication-centric applications, i.e., applications consisting of ensembles of interacting services. Services are modelled in CAT as contract automata and communication safety is defined in terms of agreement properties. With the help of a simple (albeit non trivial) example, we demonstrate how CAT can (i) verify agreement properties, (ii) synthesise an orchestrator enforcing communication safety, (iii) detect misbehaving services, and (iv) check when the services form a choreography. The use of mixed-integer linear programming is a distinguished characteristic of CAT that allows us to verify context-sensitive properties of agreement.


  1. 1.
    Arbab, F.: Reo: a channel-based coordination model for component composition. Math. Struct. Comput. Sci. 14(3), 329–366 (2004). MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Baier, C., Sirjani, M., Arbab, F., Rutten, J.: Modeling component connectors in Reo by constraint automata. Sci. Comput. Program. 61(2), 75–113 (2006). MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Basile, D.: JAMATA and CAT.
  4. 4.
    Basile, D., Degano, P., Ferrari, G.-L.: Automata for analysing service contracts. In: Maffei, M., Tuosto, E. (eds.) TGC 2014. LNCS, vol. 8902, pp. 34–50. Springer, Heidelberg (2014)Google Scholar
  5. 5.
    Basile, D., Degano, P., Ferrari, G.L., Tuosto, E.: From orchestration to choreography through contract automata. In: ICE 2014, pp. 67–85 (2014)Google Scholar
  6. 6.
    Basile, D., Degano, P., Ferrari, G.L., Tuosto, E.: Relating two automata-based models of orchestration and choreography. J. Logical Algebr. Methods Programm. 85(3), 425–446 (2016). MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems. Springer, Secaucus (2006)zbMATHGoogle Scholar
  8. 8.
    Fourer, R., Gay, D.M., Kernighan, B.W.: AMPL: A Mathematical Programming Language. AT & T Bell Laboratories Murray Hill, NJ 07974 (1987)Google Scholar
  9. 9.
    Fu, X., Bultan, T., Su, J.: Analysis of interacting BPEL web services. In: WWW 2004, pp. 621–630. ACM (2004).
  10. 10.
    Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Necula, G.C., Wadler, P. (eds.) POPL, pp. 273–284. ACM (2008)Google Scholar
  11. 11.
    Juric, M.B.: Business Process Execution Language for Web Services BPEL and BPEL4WS, 2nd edn. Packt Publishing, Birmingham (2006)Google Scholar
  12. 12.
    Tasharofi, S., Vakilian, M., Moghaddam, R.Z., Sirjani, M.: Modeling web service interactions using the coordination language reo. In: Dumas, M., Heckel, R. (eds.) WS-FM 2007. LNCS, vol. 4937, pp. 108–123. Springer, Heidelberg (2008). CrossRefGoogle Scholar
  13. 13.
    Wombacher, A., Fankhauser, P., Neuhold, E.: Transforming BPEL into annotated deterministic finite state automata for service discovery. In: Web Services (2004)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2016

Authors and Affiliations

  • Davide Basile
    • 1
    • 2
    Email author
  • Pierpaolo Degano
    • 2
  • Gian-Luigi Ferrari
    • 2
  • Emilio Tuosto
    • 3
  1. 1.I.S.T.I “A.Faedo” CNR PisaPisaItaly
  2. 2.Department of Computer ScienceUniversity of PisaPisaItaly
  3. 3.Department of Computer ScienceUniversity of LeicesterLeicesterUK

Personalised recommendations