×

zbMATH — the first resource for mathematics

Process calculi as a tool for studying coordination, contracts and session types. (English) Zbl 07189660
Summary: We recall techniques, mainly based on the theory of process calculi, that we used to prove results in twenty years of research, spanning across the old and the new millennium, on the expressiveness of coordination languages and on behavioural contracts for Service-Oriented Computing. Then, we show how such techniques recently contributed to the clarification of aspects that were unclear about session types, in particular, asynchronous session subtyping that was considered decidable since 2009, while it was proved to be undecidable in 2017.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
Linda
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Gelernter, D., Generative communication in Linda, ACM Trans. Program. Lang. Syst., 7, 1, 80-112 (1985) · Zbl 0559.68030
[2] Carriero, N.; Gelernter, D., The s/net’s Linda kernel (extended abstract), (Proc. of 10th ACM Symposium on Operating System Principles. Proc. of 10th ACM Symposium on Operating System Principles, SOSP’85 (1985), ACM), 160
[3] De Nicola, R.; Pugliese, R., A process algebra based on LINDA, (Proc. of 1st Int. Conference on Coordination Languages and Models. Proc. of 1st Int. Conference on Coordination Languages and Models, COORDINATION’96. Proc. of 1st Int. Conference on Coordination Languages and Models. Proc. of 1st Int. Conference on Coordination Languages and Models, COORDINATION’96, Lecture Notes in Computer Science, vol. 1061 (1996), Springer), 160-178
[4] Busi, N.; Gorrieri, R.; Zavattaro, G., Three semantics of the output operation for generative communication, (Proc. of 2nd Int. Conference on Coordination Languages and Models. Proc. of 2nd Int. Conference on Coordination Languages and Models, COORDINATION’97. Proc. of 2nd Int. Conference on Coordination Languages and Models. Proc. of 2nd Int. Conference on Coordination Languages and Models, COORDINATION’97, Lecture Notes in Computer Science, vol. 1282 (1997), Springer), 205-219
[5] Busi, N.; Gorrieri, R.; Zavattaro, G., On the Turing equivalence of Linda coordination primitives, (Proc. of 4th Workshop on Expressiveness in Concurrency. Proc. of 4th Workshop on Expressiveness in Concurrency, EXPRESS’97. Proc. of 4th Workshop on Expressiveness in Concurrency. Proc. of 4th Workshop on Expressiveness in Concurrency, EXPRESS’97, Electr. Notes Theor. Comput. Sci., vol. 7 (1997), Elsevier) · Zbl 0911.68139
[6] Dufourd, C.; Finkel, A.; Schnoebelen, P., Reset nets between decidability and undecidability, (Proc. of 25th Int. Colloquium on Automata, Languages and Programming. Proc. of 25th Int. Colloquium on Automata, Languages and Programming, ICALP’98. Proc. of 25th Int. Colloquium on Automata, Languages and Programming. Proc. of 25th Int. Colloquium on Automata, Languages and Programming, ICALP’98, Lecture Notes in Computer Science, vol. 1443 (1998), Springer), 103-115 · Zbl 0909.68124
[7] Busi, N.; Zavattaro, G., On the expressiveness of event notification in data-driven coordination languages, (Proc. of 9th European Symposium on Programming. Proc. of 9th European Symposium on Programming, ESOP’00. Proc. of 9th European Symposium on Programming. Proc. of 9th European Symposium on Programming, ESOP’00, Lecture Notes in Computer Science, vol. 1782 (2000), Springer), 41-55 · Zbl 0971.68655
[8] Busi, N.; Gorrieri, R.; Zavattaro, G., Temporary data in shared dataspace coordination languages, (Proc. of 4th Int. Conference on Foundations of Software Science and Computation Structures. Proc. of 4th Int. Conference on Foundations of Software Science and Computation Structures, FOSSACS’01. Proc. of 4th Int. Conference on Foundations of Software Science and Computation Structures. Proc. of 4th Int. Conference on Foundations of Software Science and Computation Structures, FOSSACS’01, Lecture Notes in Computer Science, vol. 2030 (2001), Springer), 121-136 · Zbl 0986.68098
[9] Bravetti, M.; Gilmore, S.; Guidi, C.; Tribastone, M., Replicating web services for scalability, (TGC. TGC, LNCS, vol. 4912 (2008), Springer), 204-221
[10] Carpineti, S.; Castagna, G.; Laneve, C.; Padovani, L., A formal account of contracts for web services, (Proc. of 3rd Int. Workshop on Web Services and Formal Methods. Proc. of 3rd Int. Workshop on Web Services and Formal Methods, WS-FM’06. Proc. of 3rd Int. Workshop on Web Services and Formal Methods. Proc. of 3rd Int. Workshop on Web Services and Formal Methods, WS-FM’06, Lecture Notes in Computer Science, vol. 4184 (2006), Springer), 148-162
[11] Bravetti, M.; Zavattaro, G., Contract based multi-party service composition, (Proc. of Int. Symposium on Fundamentals of Software Engineering. Proc. of Int. Symposium on Fundamentals of Software Engineering, FSEN’07. Proc. of Int. Symposium on Fundamentals of Software Engineering. Proc. of Int. Symposium on Fundamentals of Software Engineering, FSEN’07, Lecture Notes in Computer Science, vol. 4767 (2007), Springer), 207-222 · Zbl 1141.68502
[12] Bravetti, M.; Zavattaro, G., A theory for strong service compliance, (Proc. of 9th Int. Conference on Coordination Models and Languages. Proc. of 9th Int. Conference on Coordination Models and Languages, COORDINATION’07. Proc. of 9th Int. Conference on Coordination Models and Languages. Proc. of 9th Int. Conference on Coordination Models and Languages, COORDINATION’07, Lecture Notes in Computer Science, vol. 4467 (2007), Springer), 96-112
[13] Bravetti, M.; Zavattaro, G., Contract compliance and choreography conformance in the presence of message queues, (Proc. of 5th Int. Workshop on Web Services and Formal Methods. Proc. of 5th Int. Workshop on Web Services and Formal Methods, WS-FM’08. Proc. of 5th Int. Workshop on Web Services and Formal Methods. Proc. of 5th Int. Workshop on Web Services and Formal Methods, WS-FM’08, Lecture Notes in Computer Science, vol. 5387 (2008), Springer), 37-54
[14] Honda, K.; Yoshida, N.; Carbone, M., Multiparty asynchronous session types, (Proc. of 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Proc. of 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’08 (2008), ACM), 273-284 · Zbl 1295.68150
[15] Gay, S. J.; Hole, M., Subtyping for session types in the pi calculus, Acta Inform., 42, 2-3, 191-225 (2005) · Zbl 1079.68065
[16] Mostrous, D.; Yoshida, N.; Honda, K., Global principal typing in partially commutative asynchronous sessions, (Proc. of 18th European Symposium on Programming. Proc. of 18th European Symposium on Programming, ESOP’09. Proc. of 18th European Symposium on Programming. Proc. of 18th European Symposium on Programming, ESOP’09, Lecture Notes in Computer Science, vol. 5502 (2009), Springer), 316-332 · Zbl 1234.68304
[17] Bravetti, M.; Carbone, M.; Zavattaro, G., Undecidability of asynchronous session subtyping, Inf. Comput., 256, 300-320 (2017) · Zbl 1376.68098
[18] Lange, J.; Yoshida, N., On the undecidability of asynchronous session subtyping, (Proc. of 20th Int. Conference on Foundations of Software Science and Computation Structures. Proc. of 20th Int. Conference on Foundations of Software Science and Computation Structures, FOSSACS’17. Proc. of 20th Int. Conference on Foundations of Software Science and Computation Structures. Proc. of 20th Int. Conference on Foundations of Software Science and Computation Structures, FOSSACS’17, Lecture Notes in Computer Science, vol. 10203 (2017)), 441-457 · Zbl 06721005
[19] Bravetti, M.; Carbone, M.; Zavattaro, G., On the boundary between decidability and undecidability of asynchronous session subtyping, Theor. Comput. Sci., 722, 19-51 (2018) · Zbl 1388.68024
[20] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, I/II, Inf. Comput., 100, 1 (1992)
[21] Mayr, E. W., An algorithm for the general petri net reachability problem, (Proceedings of the 13th Annual ACM Symposium on Theory of Computing. Proceedings of the 13th Annual ACM Symposium on Theory of Computing, May 11-13, 1981, Milwaukee, Wisconsin, USA (1981), ACM), 238-246
[22] Rackoff, C., The covering and boundedness problems for vector addition systems, Theor. Comput. Sci., 6, 223-231 (1978) · Zbl 0368.68054
[23] Shepherdson, J. C.; Sturgis, H. E., Computability of recursive functions, J. ACM, 10, 2, 217-255 (1963) · Zbl 0118.25401
[24] Minsky, M. L., Computation: Finite and Infinite Machines (1967), Prentice-Hall, Inc. · Zbl 0195.02402
[25] Finkel, A.; Schnoebelen, P., Well-structured transition systems everywhere!, Theor. Comput. Sci., 256, 1-2, 63-92 (2001) · Zbl 0973.68170
[26] Busi, N.; Zavattaro, G., On the expressiveness of movement in pure mobile ambients, Electron. Notes Theor. Comput. Sci., 66, 3, 22-36 (2002)
[27] Fournet, C.; Hoare, C. A.R.; Rajamani, S. K.; Rehof, J., Stuck-free conformance, (Proc. of 16th International Conference on Computer Aided Verification. Proc. of 16th International Conference on Computer Aided Verification, CAV’04. Proc. of 16th International Conference on Computer Aided Verification. Proc. of 16th International Conference on Computer Aided Verification, CAV’04, Lecture Notes in Computer Science, vol. 3114 (2004), Springer), 242-254 · Zbl 1103.68612
[28] Milner, R., Communication and Concurrency (1989), Prentice Hall · Zbl 0683.68008
[29] Bravetti, M.; Zavattaro, G., Towards a unifying theory for choreography conformance and contract compliance, (Proc. of 6th Int. Symposium Software Composition. Proc. of 6th Int. Symposium Software Composition, SC’07. Proc. of 6th Int. Symposium Software Composition. Proc. of 6th Int. Symposium Software Composition, SC’07, Lecture Notes in Computer Science, vol. 4829 (2007), Springer), 34-50
[30] Laneve, C.; Padovani, L., The must preorder revisited, (Proc. of 18th Int. Conference Concurrency Theory. Proc. of 18th Int. Conference Concurrency Theory, CONCUR’07. Proc. of 18th Int. Conference Concurrency Theory. Proc. of 18th Int. Conference Concurrency Theory, CONCUR’07, Lecture Notes in Computer Science, vol. 4703 (2007), Springer), 212-225 · Zbl 1151.68319
[31] Castagna, G.; Gesbert, N.; Padovani, L., A theory of contracts for web services, (Proc. of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Proc. of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’08 (2008), ACM), 261-272 · Zbl 1295.68080
[32] Barbanera, F.; de’Liguoro, U., Two notions of sub-behaviour for session-based client/server systems, (Proc. of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming. Proc. of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP’10 (2010), ACM), 155-164
[33] Bravetti, M.; Zavattaro, G., A foundational theory of contracts for multi-party service composition, Fundam. Inform., 89, 4, 451-478 (2008) · Zbl 1154.68336
[34] Boreale, M.; Bravetti, M., Advanced mechanisms for service composition, query and discovery, (Rigorous Software Engineering for Service-Oriented Systems - Results of the SENSORIA Project on Software Engineering for Service-Oriented Computing. Rigorous Software Engineering for Service-Oriented Systems - Results of the SENSORIA Project on Software Engineering for Service-Oriented Computing, Lecture Notes in Computer Science, vol. 6582 (2011), Springer), 282-301
[35] Milner, R., A complete axiomatisation for observational congruence of finite-state behaviors, Inf. Comput., 81, 2, 227-247 (1989) · Zbl 0688.68050
[36] Bravetti, M.; Zavattaro, G., Contract-based discovery and composition of web services, (Formal Methods for Web Services, 9th International School on Formal Methods for the Design of Computer, Communication, and Software Systems. Formal Methods for Web Services, 9th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2009, vol. 5569 (2009), Springer), 261-295
[37] OASIS, Web services business process execution language version 2.0 OASIS standard
[38] Bravetti, M.; Zavattaro, G., Choreographies and behavioural contracts on the way to dynamic updates, (Proc. 1st Workshop on Logics and Model-Checking for Self-* Systems. Proc. 1st Workshop on Logics and Model-Checking for Self-* Systems, MOD*’14. Proc. 1st Workshop on Logics and Model-Checking for Self-* Systems. Proc. 1st Workshop on Logics and Model-Checking for Self-* Systems, MOD*’14, EPTCS, vol. 168 (2014)), 12-31
[39] Rensink, A.; Vogler, W., Fair testing, Inf. Comput., 205, 2, 125-198 (2007) · Zbl 1109.68077
[40] De Nicola, R.; Hennessy, M., Testing equivalences for processes, Theor. Comput. Sci., 34, 83-133 (1984) · Zbl 0985.68518
[41] Honda, K.; Vasconcelos, V. T.; Kubo, M., Language primitives and type discipline for structured communication-based programming, (Proc. of 7th European Symposium on Programming. Proc. of 7th European Symposium on Programming, ESOP’98. Proc. of 7th European Symposium on Programming. Proc. of 7th European Symposium on Programming, ESOP’98, Lecture Notes in Computer Science, vol. 1381 (1998), Springer), 122-138
[42] Lindley, S.; Morris, J. G., Embedding session types in Haskell, (Proc. of 9th International Symposium on Haskell. Proc. of 9th International Symposium on Haskell, Haskell’16 (2016)), 133-145
[43] Ng, N.; Yoshida, N., Static deadlock detection for concurrent go by global session graph synthesis, (Proc. of 25th International Conference on Compiler Construction. Proc. of 25th International Conference on Compiler Construction, CC’16 (2016)), 174-184
[44] Jespersen, T. B.L.; Munksgaard, P.; Larsen, K. F., Session types for Rust, (Proc. of 11th ACM SIGPLAN Workshop on Generic Programming. Proc. of 11th ACM SIGPLAN Workshop on Generic Programming, WGP@ICFP’15 (2015)), 13-22
[45] Mostrous, D.; Yoshida, N., Session typing and asynchronous subtyping for the higher-order π-calculus, Inf. Comput., 241, 227-263 (2015) · Zbl 1309.68139
[46] Chen, T.; Dezani-Ciancaglini, M.; Scalas, A.; Yoshida, N., On the preciseness of subtyping in session types, Log. Methods Comput. Sci., 13, 2 (2017) · Zbl 1398.68360
[47] Kozen, D., Automata and Computability (1997), Springer: Springer New York · Zbl 0883.68055
[48] Brand, D.; Zafiropulo, P., On communicating finite-state machines, J. ACM, 30, 2, 323-342 (1983) · Zbl 0512.68039
[49] Papadopoulos, G. A.; Arbab, F., Coordination models and languages, Adv. Comput., 46, 329-400 (1998)
[50] Busi, N.; Zavattaro, G., A process algebraic view of shared dataspace coordination, J. Log. Algebraic Program., 75, 1, 52-85 (2008) · Zbl 1135.68043
[51] Ancona, D.; Bono, V.; Bravetti, M.; Campos, J.; Castagna, G.; Deniélou, P.; Gay, S. J.; Gesbert, N.; Giachino, E.; Hu, R.; Johnsen, E. B.; Martins, F.; Mascardi, V.; Montesi, F.; Neykova, R.; Ng, N.; Padovani, L.; Vasconcelos, V. T.; Yoshida, N., Behavioral types in programming languages, Found. Trends Program. Lang., 3, 2-3, 95-230 (2016)
[52] Hüttel, H.; Lanese, I.; Vasconcelos, V. T.; Caires, L.; Carbone, M.; Deniélou, P.; Mostrous, D.; Padovani, L.; Ravara, A.; Tuosto, E.; Vieira, H. T.; Zavattaro, G., Foundations of session types and behavioural contracts, ACM Comput. Surv., 49, 1, 3:1-3:36 (2016)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.