Marco Carbone
Skip Abstract Section
Abstract
This article relates two different paradigms of descriptions of communication behavior, one focusing on global message flows and another on end-point behaviors, using formal calculi based on session types. The global calculus, which originates from a Web service description language (W3C WS-CDL), describes an interaction scenario from a vantage viewpoint; the end-point calculus, an applied typed π-calculus, precisely identifies a local behavior of each participant. We explore a theory of end-point projection, by which we can map a global description to its end-point counterparts preserving types and dynamics. Three principles of well-structured description and the type structures play a fundamental role in the theory.
- Abadi, M. and Fournet, C. 2001. Mobile values, new names, and secure communication. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’01). ACM Press, New York, NY, 104--115. Google Scholar
Digital Library
- Abadi, M. and Gordon, A. D. 1999. A calculus for cryptographic protocols: The SPI calculus. Inf. Comput. 148, 1, 1--70. Google ScholarDigital Library
- Alur, R., Etessami, K., and Yannakakis, M. 2005. Realizability and verification of MSC graphs. Theor. Comput. Sci. 331, 1, 97--114. Google ScholarDigital Library
- Arbab, F. 2004. Reo: A channel-based coordination model for component composition. Math. Struct. Comput. Sci. 14, 3, 329--366. Google ScholarDigital Library
- Baeten, J., van Beek, H., and Mauw, S. 2001. Specifying internet applications with DiCons. In Proceedings of the ACM Symposium on Applied Computing (SAC’01). ACM Press, New York, NY, 576--584. Google ScholarDigital Library
- Basu, A., Bozga, M., and Sifakis, J. 2006. Modeling heterogeneous real-time components in bip. In Proceedings of the International Conference on Software Engineering and Formal Methods (SEFM’06). IEEE Computer Society Press, 3--12. Google ScholarDigital Library
- Benton, N., Cardelli, L., and Fournet, C. 2004. Modern concurrency abstractions for C#. ACM Trans. Program. Lang. Syst. 26, 5, 769--804. Google ScholarDigital Library
- Berger, M., Honda, K., and Yoshida, N. 2001. Sequentiality and the π-calculus. In Proceedings of the 5th International Conference on Typed Lambda Calculi and Applications (TLCA’01). Lecture Notes in Computer Science, vol. 2044, Springer, 29--45. Google ScholarDigital Library
- Bhargavan, K., Fournet, C., and Gordon, A. D. 2006. Verified reference implementations of WS-security protocols. In Proceedings of the 3rd International Workshop on Web Services and Formal Methods (WS-FM’06). Lecture Notes in Computer Science, vol. 4184, Springer, 88--106. Google ScholarDigital Library
- Bhargavan, K., Corin, R., malo Denilou, P., Fournet, C., and Leifer, J. J. 2009. Cryptographic protocol synthesis and verification for multiparty sessions. In Proceedings of the 22nd IEEE Computer Security Foundations Symposium (CSF’09). IEEE Computer Society, 124--140. Google ScholarDigital Library
- Bonelli, E., Compagnoni, A. B., and Gunter, E. L. 2005. Correspondence assertions for process synchronization in concurrent communications. J. Funct. Program. 15, 2, 219--247. Google ScholarDigital Library
- Bravetti, M. and Zavattaro, G. 2007. A theory for strong service compliance. In Proceedings of the 8th International Conference on Coordination Models and Languages (COORDINATION’07). Lecture Notes in Computer Science, vol. 4467, Springer, 96--112. Google ScholarDigital Library
- Briais, S. and Nestmann, U. 2005. A formal semantics for protocol narrations. In Proceedings of the 1st Symposium on Trustworthy Global Computing (TGC’05). Lecture Notes in Computer Science, vol. 3705, Springer, 163--181. Google ScholarDigital Library
- Broy, M. 2005. A semantic and methodological essence of message sequence charts. Sci. Comput. Program. 54, 2--3, 213--256. Google ScholarDigital Library
- Broy, M. 2007. Interaction and realizability. In Proceedings of the 33rd Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM’07). Springer, 29--50. Google ScholarDigital Library
- Broy, M., Krüger, I. H., and Meisinger, M. 2007. A formal model of services. ACM Trans. Softw. Engin. Method. 16, 1, 5. Google ScholarDigital Library
- Busi, N., Gorrieri, R., Guidi, C., Lucchi, R., and Zavattaro, G. 2006. Choreography and orchestration conformance for system design. In Proceedings of the 7th International Conference on Coordination Models and Languages (COORDINATION’06). Lecture Notes in Computer Science, vol. 4038, Springer, 63--81. Google ScholarDigital Library
- Caires, L. and Vieira, H. T. 2009. Conversation types. In Proceedings of the 18th European Symposium on Programming (ESOP’09). Lecture Notes in Computer Science, vol. 5502, Springer, 285--300. Google ScholarDigital Library
- Carbone, M., Nielsen, M., and Sassone, V. 2004. A calculus for trust management. In Proceedings of the 24th International Conference on Foundations of Software Technology and Theoretical Computer Science (FST-TCS’04). Lecture Notes in Computer Science, vol. 3328, Springer, 161--173. Google ScholarDigital Library
- Carbone, M., Honda, K., and Yoshida, N. 2006a. A calculus of global interaction based on session types. In Proceedings of the 2nd Workshop on Developments in Computational Models (DCM’06). Elsevier Science Publishers, Amsterdam, The Netherlands.Google Scholar
- Carbone, M., Honda, K., Yoshida, N., Milner, R., Brown, G., and Ross-Talbot, S. 2006b. A theoretical basis of communication-centred concurrent programming. W3C working note. http://www.dcs.qmul.ac.uk/~carbonem/cdlpaper/workingnote.pdf.Google Scholar
- Carbone, M., Honda, K., and Yoshida, N. 2007. Structured communication-centred programming for web services. In Proceedings of the 16th European Symposium on Programming (ESOP’07). Lecture Notes in Computer Science, vol. 4421, Springer, 2--17. Google ScholarDigital Library
- Castagna, G., Gesbert, N., and Padovani, L. 2008. A theory of contracts for web services. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’08). ACM Press, New York, NY, 261--272. Google ScholarDigital Library
- Chaki, S., Rajamani, S. K., and Rehof, J. 2002. Types as models: model checking message-passing programs. In Proceedings of the 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’02). ACM Press, New York, NY, 45--57. Google ScholarDigital Library
- Corin, R., Denièlou, P.-M., Fournet, C., Bhargavan, K., and Leifer, J. 2007. Secure implementations for typed session abstractions. In Proceedings of the 20th IEEE Computer Security Foundations Symposium (CSF’07). IEEE Computer Society Press, 170--186. Google ScholarDigital Library
- Demangeon, R. and Honda, K. 2011. Full abstraction in a subtyped pi-calculus with linear types. In Proceedings of the International Conference on Concurrency Theory (CONCUR’11). J.-P. Katoen and B. König Eds., Lecture Notes in Computer Science Series, vol. 6901, Springer, 280--296. Google ScholarDigital Library
- Dezani-Ciancaglini, M. and de’ Liguoro, U. 2009. Sessions and session types: An overview. In Proceedings of the 6th International Workshop on Web Services and Formal Methods (WS-FM’09). Google ScholarDigital Library
- Dezani-Ciancaglini, M., Mostrous, D., Yoshida, N., and Drossopoulou, S. 2006. Session types for object-oriented languages. In Proceedings of the 20th European Conference on Object-Oriented Programming (ECOOP’06). Lecture Notes in Computer Science, vol. 4067, Springer, 328--352. Google ScholarDigital Library
- Fähndrich, M., Aiken, M., Hawblitzel, C., Hodson, O., Hunt, G. C., Larus, J. R., and Levi, S. 2006. Language support for fast and reliable message-based communication in singularity OS. In Proceedings of EuroSys’06. W. Zwaenepoel Ed., ACM SIGOPS. ACM Press, 177--190. Google ScholarDigital Library
- Foster, H., Magee, J., Kramer, J., and Uchitel, S. 2010. LTSA WS-engineer home page. http://www.doc.ic.ac.uk/ltsa/bpel4ws.Google Scholar
- Fu, X., Bultan, T., and Su, J. 2004. Conversation protocols: A formalism for specification and verification of reactive electronic services. Theor. Comput. Sci. 328, 1--2, 19--37. Google ScholarDigital Library
- Fu, X., Bultan, T., and Su, J. 2005. Realizability of conversation protocols with message contents. Int. J. Web Service Resear. 2, 4, 68--93.Google ScholarCross Ref
- Gay, S. and Hole, M. 2005. Subtyping for session types in the pi calculus. Acta Informatica 42, 2--3, 191--225. Google ScholarCross Ref
- Gordon, A. D. and Pucella, R. 2002. Validating a web service security abstraction by typing. In Proceedings of the ACM Workshop on XML Security (XMLSEC’02). ACM Press, New York, NY, 18--29. Google ScholarDigital Library
- Guidi, C., Lucchi, R., Zavattaro, G., Busi, N., and Gorrieri, R. 2006. SOCK: A calculus for service oriented computing. In Proceedings of the 4th International Conference on Service Oriented Computing (ICSOC’06). Lecture Notes in Computer Science, vol. 4294, Springer, 327--338. Google ScholarDigital Library
- Guttman, J. D., Thayer, F. J., and Zuck, L. D. 2001. The faithfulness of abstract protocol analysis: message authentication. In Proceedings of the 8th ACM Conference on Computer and Communications Security (CCS’01). ACM Press, New York, NY, 186--195. Google ScholarDigital Library
- Hennessy, M. and Riely, J. 1998. Resource access control in systems of mobile agents. In Proceedings of the International Workshop on High-Level Concurrent Languages (HLCL’98). ENTCS Series, vol. 16.3. Elsevier Science Publishers, Amsterdam, The Netherlands. 3--17.Google Scholar
- Henriksen, J. G., Mukund, M., Kumar, K. N., Sohoni, M. A., and Thiagarajan, P. S. 2005. A theory of regular MSC languages. Inf. Comput. 202, 1, 1--38. Google ScholarDigital Library
- Hoare, T. 1985. Communicating Sequential Processes. Prentice Hall, UK. Google ScholarDigital Library
- Honda, K. 1996. Composing processes. In Proceedings of the 23th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’96). ACM Press, New York, NY, 344--357. Google ScholarDigital Library
- Honda, K., Vasconcelos, V., and Kubo, M. 1998. Language primitives and type disciplines for structured communication-based programming. In Proceedings of the 7th European Symposium on Programming (ESOP’98). Lecture Notes in Computer Science, vol. 1381, Springer, 22--138. Google ScholarDigital Library
- Honda, K., Yoshida, N., and Carbone, M. 2007. Web Services, mobile processes and types. Bull. Eur. Assoc. Theor. Comput. Sci. 91, 165--185.Google Scholar
- Honda, K., Yoshida, N., and Carbone, M. 2008. Multiparty asynchronous session types. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’08). ACM Press, New York, NY, 273--284. Google ScholarDigital Library
- IBM. 2001. Web services flow language (WSFL 1.0). http://www-3.ibm.com/software/solutions/webservices/pdf/WSFL.pdf.Google Scholar
- IBM. 2010. WebSphere MQ workflow. www-306.ibm.com/software/integration/wmqwf/.Google Scholar
- Igarashi, A. and Kobayashi, N. 2001. A generic type system for the pi-calculus. In Proceedings of the 28th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’01). ACM Press, New York, NY, 128--141. Google ScholarDigital Library
- International Telecommunication Union. 1996. Recommendation Z.120: Message sequence chart.Google Scholar
- Kobayashi, N., Pierce, B., and Turner, D. 1996. Linear types and π-calculus. In Proceedings of the 23th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’96). ACM Press, New York, NY, 358--371. Google ScholarDigital Library
- Laneve, C. and Padovani, L. 2006. Smooth orchestrators. In Proceedings of the 9th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS’06). Lecture Notes in Computer Science, vol. 3921, Springer, 32--46. Google ScholarDigital Library
- Microsoft. 2001. XLANG: Web services for business process design. http://www.gotdotnet.com/team/xml wsspecs/xlang-c/default.htm.Google Scholar
- Milner, R. 1993. The polyadic π-calculus: A tutorial. In Logic and Algebra of Specification, Springer.Google Scholar
- Milner, R., Parrow, J., and Walker, D. 1992. A calculus of mobile processes, I and II. Inf. Comput. 100, 1, 1--40, 41--77. Google ScholarDigital Library
- Needham, R. M. and Schroeder, M. D. 1978. Using encryption for authentication in large networks of computers. Com. ACM 21, 12, 993--999. Google ScholarDigital Library
- O’Hanlon, C. 2006. Conversation with Steve Ross-Talbot.Google Scholar
- OMG. 2004. Unified modelling language, version 2.0.Google Scholar
- PI4SOA. 2008. http://www.pi4soa.org.Google Scholar
- Pierce, B. C. 2002. Types and Programming Languages. MIT Press, Cambridge, MA. Google ScholarDigital Library
- Pierce, B. C. and Sangiorgi, D. 1996. Typing and subtyping for mobile processes. Math. Struct. Comput. Sci. 6, 5, 409--453.Google ScholarCross Ref
- Pierce, B. C. and Turner, D. N. 2000. Pict: A programming language based on the pi-calculus. In Proof, Language and Interaction: Essays in Honour of Robin Milner, MIT Press, Cambridge, MA. Google ScholarDigital Library
- Qiu, Z., Zhao, X., Cai, C., and Yang, H. 2007. Towards the theoretical foundation of choreography. In Proceedings of the International World Wide Web Conference. IEEE Computer Society Press, 973--982. Google ScholarDigital Library
- Rajamani, S. K. and Rehof, J. 2002. Conformance checking for models of asynchronous message passing software. In Proceedings of the 14th Conference on Computer-Aided Verification (CAV’02). Lecture Notes in Computer Science, vol. 2404, Springer, 166--179. Google ScholarDigital Library
- Ross-Talbot, S. and Fletcher, T. 2006. WS-CDL Primer. Published by W3C.Google Scholar
- Sangiorgi, D. 1999. The name discipline of uniform receptiveness. Theor. Comput. Sci. 221, 1--2, 457--493. Google ScholarDigital Library
- Takeuchi, K., Honda, K., and Kubo, M. 1994. An interaction-based language and its typing system. In Proceedings of the 6th International Conference on Parallel Architectures and Languages (PARLE’94). Lecture Notes in Computer Science Series, vol. 817, Springer, 398--413. Google ScholarDigital Library
- van der Aalst, W. 2002. Inheritance of interorganizational workflows: How to agree to disagree without loosing control? Info. Tech. Manage. J. 2, 3, 195--231. Google ScholarDigital Library
- Vasconcelos, V., Ravara, A., and Gay, S. J. 2004. Session types for functional multithreading. In Proceedings of the 15th International Conference on Concurrency Theory (CONCUR’04). Lecture Notes in Computer Science, vol. 3170, Springer, 497--511.Google ScholarCross Ref
- Vieira, H. T., Caires, L., and Seco, J. C. 2008. The conversation calculus: A model of service-oriented computation. In Proceedings of the 17th European Symposium on Programming (ESOP’08). Vol. 4960, Springer, 269--283. Google ScholarDigital Library
- W3C WS-CDL Working Group. 2004. Web services choreography description language version 1.0. http://www.w3.org/TR/2004/WD-ws-cdl-10-20040427/.Google Scholar
- WFMC. 2010. Workflow management coalition. http://www.wfmc.org/.Google Scholar
- Yoshida, N. 1996. Graph types for monadic mobile processes. In Proceedings of the 16th Conference on Foundations of Software Technology and Theoretical Computer Science. Springer, 371--386. Google ScholarDigital Library
- Yoshida, N. and Vasconcelos, V. 2007. Language primitives and type discipline for structured communication-based programming revisited: Two systems for higher-order session communication. Electr. Notes Theor. Comput. Sci. 171, 4, 73--93. Google ScholarDigital Library
- Yoshida, N., Berger, M., and Honda, K. 2004. Strong normalisation in the π-calculus. Inf. Comput. 191, 145--202. Google ScholarDigital Library
Index Terms
- Structured Communication-Centered Programming for Web Services
Recommendations
Theoretical Aspects of Communication-Centred Programming
This short note outlines two different ways of describing communication-centric software in the form of formal calculi and discuss their relationship. Two different paradigms of description, one centring on global message flows and another centring on ...
Web services choreography and orchestration in Reo and constraint automata
SAC '07: Proceedings of the 2007 ACM symposium on Applied computingCurrently web services constitute one of the most important topics in the realm of the World Wide Web. Composition of web services lets developers create applications on top of service-oriented computing platforms. Current web services choreography and ...
Structured communication-centred programming for web services
ESOP'07: Proceedings of the 16th European Symposium on ProgrammingThis paper relates two different paradigms of descriptions of communication behaviour, one focussing on global message flows and another on end-point behaviours, using formal calculi based on session types. The global calculus, which originates from a ...
Comments