Abstract
This paper introduces global session nets, an integration of multiparty session types (MPST) and Petri nets, for role-based choreographic specifications to verify distributed multiparty systems. The graphical representation of session nets enables more liberal combinations of branch, merge, fork and join patterns than the standard syntactic MPST. We use session net token dynamics to verify a flexible conformance between the graphical global net and syntactic endpoint types, and apply the conformance to ensure type-safety and progress of endpoint processes with channel mobility. We have implemented Java APIs for validating global session graph well-formedness and endpoint type conformance.
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
Basu, S., Bultan, T., Ouederni, M.: Deciding choreography realizability. In POPL, pp. 191–202. ACM (2012)
Bettini, L., Coppo, M., D’Antoni, L., De Luca, M., Dezani-Ciancaglini, M., Yoshida, N.: 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)
Business Process Model and Notation. http://www.bpmn.org
Castagna, G., Dezani-Ciancaglini, M., Padovani, L.: On global types and multi-party sessions. Logical Methods in Computer Science 8(1) (2012)
Castagna, G, Gesbert, N., Padovani, L.: A theory of contracts for web services. In POPL, pp. 261–272. ACM (2008)
Chen, T.-C., Honda, K.: Specifying stateful asynchronous properties for distributed programs. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 209–224. Springer, Heidelberg (2012)
CPN Homepage. http://cpntools.org/
Demangeon, R., Honda, K.: Full abstraction in a subtyped pi-calculus with linear types. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 280–296. Springer, Heidelberg (2011)
Deniélou, P.-M., Yoshida, N.: Multiparty session types meet communicating automata. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 194–213. Springer, Heidelberg (2012)
Desel, J., Esparza, J.: Free Choice Petri Nets (Cambridge Tracts in Theoretical Computer Science). Cambridge University Press (1995)
Hallé, S., Bultan, T., Hughes, G., Alkhalaf, M., Villemaire, R.: Runtime verification of web service interface contracts. Computer 43(3), 59–66 (2010)
Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In POPL, pp. 273–284. ACM (2008)
Hu, R., Yoshida, N., Honda, K.: Session-Based Distributed Programming in Java. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 516–541. Springer, Heidelberg (2008)
Lohmann, N., Massuthe, P., Stahl, C., Weinberg, D.: Analyzing interacting BPEL processes. In: Dustdar, S., Fiadeiro, J.L., Sheth, A.P. (eds.) BPM 2006. LNCS, vol. 4102, pp. 17–32. Springer, Heidelberg (2006)
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)
Murata, T.: Petri nets: properties, analysis and applications. Proceedings of the IEEE 77(4), 541–580 (1989)
OMG. Unified Modelling Language, Version 2.0 (2004)
Java APIs for session nets. http://www.doc.ic.ac.uk/~rhu/session_nets.html
Technical Report, Department of Computing, Imperial College London, May 2014. 2014/5
van der Aalst, W.M.P.: Verification of workflow nets. In: Azéma, Pierre, Balbo, Gianfranco (eds.) ICATPN 1997. LNCS, vol. 1248. Springer, Heidelberg (1997)
van der Aalst, W.M.P., Dumas, M., Ouyang, C., Rozinat, A., Verbeek, H.M.W.: Choreography conformance checking: An approach based on bpel and petri nets. In: The Role of Business Processes in Service Oriented Architectures. IBFI (2006)
van der Aalst, W.M.P., et al.: Multiparty contracts: Agreeing and implementing interorganizational processes. Comput. J. 53(1), 90–106 (2010)
Vasconcelos, V.T., Honda, K.: Principal typing scheme for polyadic \(\pi \)-calculus. In: Best, Eike (ed.) CONCUR 1993. LNCS, vol. 715. Springer, Heidelberg (1993)
Workflow Patterns homepage. http://www.workflowpatterns.com/
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fossati, L., Hu, R., Yoshida, N. (2014). Multiparty Session Nets. In: Maffei, M., Tuosto, E. (eds) Trustworthy Global Computing. TGC 2014. Lecture Notes in Computer Science(), vol 8902. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-45917-1_8
Download citation
DOI: https://doi.org/10.1007/978-3-662-45917-1_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-45916-4
Online ISBN: 978-3-662-45917-1
eBook Packages: Computer ScienceComputer Science (R0)