Abstract
In this paper we discuss our ongoing endeavour to apply notations and algorithms based on the π-calculus and its theories for the development of large-scale distributed systems. The execution of a large-scale distributed system consists of many structured conversations (or sessions) whose protocols can be clearly and accurately specified using a theory of types for the π-calculus, called session types. The proposed methodology promotes a formally founded, and highly structured, development framework for modelling and building distributed applications, from high-level models to design and implementation to static checking to runtime validation. At the centre of this methodology is a formal description language for representing protocols for interactions, called Scribble. We illustrate the usage and theoretical basis of this language through use cases from different application domains.
This work is partially supported by EPSRC EP/F003757, EP/F002114, EP/G015635 and EP/G015481.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Agha, G.: Actors: a model of concurrent computation in distributed systems. MIT Press, Cambridge (1986)
Armstrong, J.: Programming Erlang: Software for a Concurrent World. Pragmatic Bookshelf (2007)
Baeton, J., Wejland, W.: Process Algebra. Cambridge University Press, Cambridge (1990)
Baumann, A., et al.: The multikernel: a new os architecture for scalable multicore systems. In: SOSP, pp. 29–44. ACM, New York (2009)
Baumann, A., Peter, S., Schüpbach, A., Singhania, A., Roscoe, T., Barham, P., Isaacs, R.: Your computer is already a distributed system. why isn’t your os? In: Proceedings of the 12th Conference on Hot Topics in Operating Systems, HotOS 2009, pp. 12. USENIX Association, Berkeley (2009)
Bettini, L., et al.: Global progress in dynamically interleaved multiparty sessions. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 418–433. Springer, Heidelberg (2008)
Bhargavan, K., Corin, R., Deniélou, P.-M., Fournet, C., Leifer, J.: Cryptographic protocol synthesis and verification for multiparty sessions. In: CSF, pp. 124–140 (2009)
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)
Broy, M., Krüger, I.H., Meisinger, M.: A formal model of services. ACM Trans. Softw. Eng. Methodol. 16(1), 5 (2007)
Capecchi, S., Castellani, I., Dezani-Ciancaglini, M., Rezk, T.: Session Types for Access and Information Flow Control. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 237–252. Springer, Heidelberg (2010)
Capecchi, S., Giachino, E., Yoshida, N.: Global escape in multiparty session. In: FSTTCS 2010 (2010) (to appear), http://www.di.unito.it/~capecchi/mpe.pdf
Carbone, M., Honda, K., Yoshida, N.: Structured Communication-Centred Programming for Web Services. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 2–17. Springer, Heidelberg (2007)
W3C Web Services Choreography Description Language, http://www.w3.org/2002/ws/chor/
Chave, A., Arrott, M., Farcas, C., Farcas, E., Krueger, I., Meisinger, M., Orcutt, J., Vernon, F., Peach, C., Schofield, O., Kleinert, J.: Cyberinfrastructure for the US Ocean Observatories Initiative. In: Proc. IEEE OCEANS 2009. IEEE, Los Alamitos (2009)
Damas, L., Milner, R.: Principal type-schemes for functional programs. In: POPL, pp. 207–212 (1982)
Deniélou, P.-M., Yoshida, N.: Buffered communication analysis in distributed multiparty sessions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 343–357. Springer, Heidelberg (2010) Full version, Prototype at, http://www.doc.ic.ac.uk/~pmalo/multianalysis
Deniélou, P.-M., Yoshida, N.: Dynamic multirole session types. In: POPL 2011. ACM, New York (2011) (to appear), http://www.doc.ic.ac.uk/~malo/dynamic
Desai, N., Chopra, A.K., Arrott, M., Specht, B., Singh, M.P.: Engineering foreign exchange processes via commitment protocols. In: IEEE SCC, pp. 514–521 (2007)
Dezani-Ciancaglini, M., Mostrous, D., Yoshida, N., Gairing, M.: Session Types for Object-Oriented Languages. In: Hu, Q. (ed.) ECOOP 2006. LNCS, vol. 4067, pp. 328–352. Springer, Heidelberg (2006)
Frankel, D.S.: Model Driven Architecture: Applying MDA to Enterprise Computing. Wiley, Chichester (January 2003)
Hoare, T.: An axiomatic basis of computer programming. CACM 12 (1969)
Hoare, T.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)
Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type disciplines for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122–138. Springer, Heidelberg (1998)
Honda, K., Yoshida, N., Carbone, M.: Multiparty Asynchronous Session Types. In: POPL 2008, pp. 273–284. ACM, New York (2008)
Hu, R., Kouzapas, D., Pernet, O., Yoshida, N., Honda, K.: Type-safe eventful sessions in Java. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 329–353. Springer, Heidelberg (2010)
Hu, R., Yoshida, N., Macko, M.: Session-Based Distributed Programming in Java. In: Ryan, M. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 516–541. Springer, Heidelberg (2008)
International Telecommunication Union. Recommendation Z.120: Message sequence chart (1996)
Meyer, B.: Applying “Design by Contract”. Computer 25(10), 40–51 (1992)
Milner, R.: Theory of type polymorphism in programming languages. In: TCS (1982)
Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, Parts I and II. Info. & Comp. 100(1) (1992)
Mostrous, D., Yoshida, N., Honda, K.: Global principal typing in partially commutative asynchronous sessions. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 316–332. Springer, Heidelberg (2009)
Ng, N.: High performance parallel design based on session programming. Masters thesis, Department of Computing, Imperial College London (2010), http://www.doc.ic.ac.uk/~cn06/individual-project/
Nielsen, L., Yoshida, N., Honda, K.: Multiparty symmetric sumtypes. Technical Report 8, Department of Computing, Imperial College London (2009), To appear in Express’10. Apims Project at, http://www.thelas.dk/index.php/apims
OMG. Unified Modelling Language, Version 2.0 (2004)
Ocean Observatories Initiative (OOI), http://www.oceanleadership.org/programs-andartnerships/ocean-observing/ooi/
pi4soa homepage, http://pi4soa.sourceforge.net/
Scribble development tool site, http://www.jboss.org/scribble
Sivaramakrishnan, K.C., Nagaraj, K., Ziarek, L., Eugster, P.: Efficient session type guided distributed interaction. In: Clarke, D., Agha, G. (eds.) COORDINATION 2010. LNCS, vol. 6116, pp. 152–167. Springer, Heidelberg (2010)
Takeuchi, K., Honda, K., Kubo, M.: An Interaction-based Language and its Typing System. In: Halatsis, C., Philokyprou, G., Maritsas, D., Theodoridis, S. (eds.) PARLE 1994. LNCS, vol. 817, pp. 398–413. Springer, Heidelberg (1994)
Trivedi, A.: Hotplug in a multikernel operating system. Master’s thesis, ETH Zurich (2009)
UNIFI. International Organization for Standardization ISO 20022 UNIversal Financial Industry message scheme (2002), http://www.iso20022.org
Welch, P., Barnes, F.: Communicating Mobile Processes: introducing occam-pi. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.) CSP 2004. LNCS, vol. 3525, pp. 175–210. Springer, Heidelberg (2005)
Yoshida, N., Deniélou, P.-M., Bejleri, A., Hu, R.: Parameterised multiparty session types. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 128–145. Springer, Heidelberg (2010)
Yoshida, N., Vasconcelos, V.T., Paulino, H., Honda, K.: Session-based compilation framework for multicore programming. In: de Boer, F.S., Bonsangue, M.M., Madelaine, E. (eds.) FMCO 2008. LNCS, vol. 5751, pp. 226–246. Springer, Heidelberg (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Honda, K., Mukhamedov, A., Brown, G., Chen, TC., Yoshida, N. (2011). Scribbling Interactions with a Formal Foundation. In: Natarajan, R., Ojo, A. (eds) Distributed Computing and Internet Technology. ICDCIT 2011. Lecture Notes in Computer Science, vol 6536. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19056-8_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-19056-8_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19055-1
Online ISBN: 978-3-642-19056-8
eBook Packages: Computer ScienceComputer Science (R0)