Enforcing Availability in Failure-Aware Communicating Systems

  • Hugo A. LópezEmail author
  • Flemming NielsonEmail author
  • Hanne Riis NielsonEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9688)


Choreographic programming is a programming-language design approach that drives error-safe protocol development in distributed systems. Motivated by challenging scenarios in Cyber-Physical Systems (CPS), we study how choreographic programming can cater for dynamic infrastructures where the availability of components may change at runtime. We introduce the Global Quality Calculus (\(GC_q\)), a process calculus featuring novel operators for multiparty, partial and collective communications; we provide a type discipline that controls how partial communications refer only to available components; and we show that well-typed choreographies enjoy progress.



We would like to thank Marco Carbone and Jorge A. Pérez for their insightful discussions, and to all anonymous reviewers for their helpful comments improving the paper. This research was funded by the Danish Foundation for Basic Research, project IDEA4CPS (DNRF86-10). López has benefitted from travel support by the EU COST Action IC1201: Behavioural Types for Reliable Large-Scale Software Systems (BETTY).

Supplementary material


  1. 1.
    Abdulla, P.A., Atig, M.F., Meyer, R., Salehi, M.S.: What’s decidable about availability languages? In: Harsha, P., Ramalingam, G. (eds.) FSTTCS. LIPIcs, vol. 45, pp. 192–205. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)Google Scholar
  2. 2.
    Alur, R.: Principles of Cyber-Physical Systems. MIT Press, Cambridge (2015)Google Scholar
  3. 3.
    Bocchi, L., Chen, T.-C., Demangeon, R., Honda, K., Yoshida, N.: Monitoring networks through multiparty session types. In: Beyer, D., Boreale, M. (eds.) FORTE 2013 and FMOODS 2013. LNCS, vol. 7892, pp. 50–65. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  4. 4.
    Bocchi, L., Honda, K., Tuosto, E., Yoshida, N.: A theory of design-by-contract for distributed multiparty interactions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 162–176. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  5. 5.
    Bocchi, L., Lange, J., Yoshida, N.: Meeting deadlines together. In: Aceto, L., de Frutos-Escrig, D. (eds.) CONCUR, LIPIcs, vol. 42, pp. 283–296. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)Google Scholar
  6. 6.
    Bocchi, L., Yang, W., Yoshida, N.: Timed multiparty session types. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 419–434. Springer, Heidelberg (2014)Google Scholar
  7. 7.
    Carbone, M.: Session-based choreography with exceptions. Electron. Notes Theor. Comput. Sci. 241, 35–55 (2009)CrossRefGoogle Scholar
  8. 8.
    Carbone, M., Honda, K., Yoshida, N.: Structured interactional exceptions in session types. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 402–417. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  9. 9.
    Carbone, M., Honda, K., Yoshida, N.: Structured communication-centered programming for web services. ACM Trans. Program. Lang. Syst. 34(2), 8 (2012)CrossRefzbMATHGoogle Scholar
  10. 10.
    Carbone, M., Honda, K., Yoshida, N., Milner, R., Brown, G., Ross-Talbot, S.: A theoretical basis of communication-centred concurrent programming. In: Web Services Choreography Working Group mailing list, WS-CDL working report (2006, to appear)Google Scholar
  11. 11.
    Carbone, M., Montesi, F.: Chor: a choreography programming language for concurrent systems.
  12. 12.
    Carbone, M., Montesi, F.: Deadlock-freedom-by-design: multiparty asynchronous global programming. In: Giacobazzi, R., Cousot, R. (eds.) POPL, pp. 263–274. ACM (2013)Google Scholar
  13. 13.
    Castagna, G., Dezani-Ciancaglini, M., Padovani, L.: On global types and multi-party session. Logical Methods Comput. Sci. 8(1), 1–45 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Cogumbreiro, T., Martins, F., Thudichum Vasconcelos, V.: Coordinating phased activities while maintaining progress. In: De Nicola, R., Julien, C. (eds.) COORDINATION 2013. LNCS, vol. 7890, pp. 31–44. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  15. 15.
    Deng, J., Han, Y.S., Heinzelman, W.B., Varshney, P.K.: Balanced-energy sleep scheduling scheme for high-density cluster-based sensor networks. Comput. Commun. 28(14), 1631–1642 (2005)CrossRefGoogle Scholar
  16. 16.
    Deniélou, P.-M., Yoshida, N.: Multiparty session types meet communicating automata. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 194–213. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  17. 17.
    Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Harper, R.: Programming in Standard ML. Working Draft (2013)Google Scholar
  19. 19.
    Heinzelman, W.B., Chandrakasan, A.P., Balakrishnan, H.: An application-specific protocol architecture for wireless microsensor networks. IEEE Trans. Wireless Commun. 1(4), 660–670 (2002)CrossRefGoogle Scholar
  20. 20.
    Heinzelman, W.R., Kulik, J., Balakrishnan, H.: Adaptive protocols for information dissemination in wireless sensor networks. In MOBICOM, pp. 174–185. ACM (1999)Google Scholar
  21. 21.
    Hoare, C.A.R.: An axiomatic basis for computer programming (reprint). Commun. ACM 26(1), 53–56 (1983)MathSciNetCrossRefGoogle Scholar
  22. 22.
    Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122–138. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  23. 23.
    Hüttel, H., Pratas, N.: Broadcast and aggregation in BBC. In: Gay, S., Alglave, J. (eds.) PLACES, EPTCS, pp. 51–62 (2015)Google Scholar
  24. 24.
    Intanagonwiwat, C., Govindan, R., Estrin, D.: Directed diffusion: a scalable and robust communication paradigm for sensor networks. In: Pickholtz, R.L., Das, S.K., Cáceres, R., Garcia-Luna-Aceves, J.J. (eds.) MOBICOM, pp. 56–67. ACM (2000)Google Scholar
  25. 25.
    Kouzapas, D., Gutkovas, R., Gay, S.J.: Session types for broadcasting. In: Donaldson, A.F., Vasconcelos, V.T. (eds.) PLACES, EPTCS, vol. 155, pp. 25–31 (2014)Google Scholar
  26. 26.
    Lincoln, P.: Deciding provability of linear logic formulas. In: Advances in Linear Logic, pp. 109–122. Cambridge University Press (1994)Google Scholar
  27. 27.
    López, H.A., Marques, E.R.B., Martins, F., Ng, N., Santos, C., Vasconcelos, V.T., Yoshida, N.: Protocol-based verification of message-passing parallel programs. In: Aldrich, J., Eugster, P. (eds.) OOPSLA, pp. 280–298. ACM (2015)Google Scholar
  28. 28.
    López, H.A., Pérez, J.A.: Time and exceptional behavior in multiparty structured interactions. In: Carbone, M., Petit, J.-M. (eds.) WS-FM 2011. LNCS, vol. 7176, pp. 48–63. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  29. 29.
    Madden, S., Franklin, M.J., Hellerstein, J.M., Hong, W.: TAG: A tiny aggregation service for ad-hoc sensor networks. In: Culler, D.E., Druschel, P. (eds.) OSDI. USENIX Association (2002)Google Scholar
  30. 30.
    Madden, S., Franklin, M.J., Hellerstein, J.M., Hong, W.: The design of an acquisitional query processor for sensor networks. In: Halevy, A.Y., Ives, Z.G., Doan, A. (eds.) SIGMOD Conference, pp. 491–502. ACM (2003)Google Scholar
  31. 31.
    Montesi, F., Guidi, C., Zavattaro, G.: Service-oriented programming with jolie. In: Bouguettaya, A., Sheng, Q.Z., Daniel, F. (eds.) Web Services Foundations, pp. 81–107. Springer, New York (2014)CrossRefGoogle Scholar
  32. 32.
    Neykova, R., Bocchi, L., Yoshida, N.: Timed runtime monitoring for multiparty conversations. In: Carbone, M. (ed.) BEAT, EPTCS, vol. 162, pp. 19–26 (2014)Google Scholar
  33. 33.
    Nielson, H.R., Nielson, F., Vigo, R.: A calculus for quality. In: Păsăreanu, C.S., Salaün, G. (eds.) FACS 2012. LNCS, vol. 7684, pp. 188–204. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  34. 34.
    Pattem, S., Krishnamachari, B., Govindan, R.: The impact of spatial correlation on routing with compression in wireless sensor networks. TOSN 4(4), 1–23 (2008)CrossRefGoogle Scholar
  35. 35.
    Perillo, M.A., Heinzelman, W.B.: Wireless sensor network protocols. In: Boukerche, A. (ed.) Handbook of Algorithms for Wireless Networking and Mobile Computing, pp. 1–35. Chapman and Hall/CRC, London (2005)Google Scholar
  36. 36.
    Yoshida, N., Hu, R., Neykova, R., Ng, N.: The Scribble Protocol Language. In: Abadi, M., Lluch Lafuente, A. (eds.) TGC 2013. LNCS, vol. 8358, pp. 22–41. Springer, Heidelberg (2014)CrossRefGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2016

Authors and Affiliations

  1. 1.Technical University of DenmarkKongens LyngbyDenmark

Personalised recommendations