skip to main content
10.1145/2676726.2676964acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

From Communicating Machines to Graphical Choreographies

Published: 14 January 2015 Publication History

Abstract

Graphical choreographies, or global graphs, are general multiparty session specifications featuring expressive constructs such as forking, merging, and joining for representing application-level protocols. Global graphs can be directly translated into modelling notations such as BPMN and UML. This paper presents an algorithm whereby a global graph can be constructed from asynchronous interactions represented by communicating finite-state machines (CFSMs). Our results include: a sound and complete characterisation of a subset of safe CFSMs from which global graphs can be constructed; an algorithm to translate CFSMs to global graphs; a time complexity analysis; and an implementation of our theory, as well as an experimental evaluation.

Supplementary Material

MPG File (p221-sidebyside.mpg)

References

[1]
Business Process Model and Notation. http://www.bpmn.org.
[2]
Petrify. http://www.lsi.upc.edu/?jordicf/petrify/.
[3]
SAVARA Testable Architecture. http://www.jboss.org/savara.
[4]
Zero Deviation Lifecycle. http://www.zdlc.co.
[5]
Full version of this paper. http://www.doc.ic.ac.uk/~jlange/papers/lty15.pdf, 2014.
[6]
GMC-Synthesis. https://bitbucket.org/julien-lange/ gmc-synthesis, 2014.
[7]
R. Alur, K. Etessami, and M. Yannakakis. Inference of Message Sequence Charts. IEEE Trans. Software Eng., 29(7):623--633, 2003.
[8]
E. Badouel and P. Darondeau. Theory of regions. In Petri Nets, volume 1491 of LNCS, pages 529--586. Springer, 1996.
[9]
C. Baier, J. Klein, and S. Klüppelholz. Synthesis of reo connectors for strategies and controllers. Fundam. Inform., 130(1):1--20, 2014.
[10]
S. Basu and T. Bultan. Choreography conformance via synchronizability. In WWW, pages 795--804. ACM, 2011.
[11]
S. Basu, T. Bultan, and M. Ouederni. Synchronizability for verification of asynchronously communicating systems. In VMCAI, volume 7148 of LNCS. Springer, 2012.
[12]
S. Basu, T. Bultan, and M. Ouederni. Deciding choreography realizability. In POPL, pages 191--202. ACM, 2012.
[13]
F. Bonchi and D. Pous. Checking nfa equivalence with bisimulations up to congruence. In POPL, pages 457--468. ACM, 2013.
[14]
D. Brand and P. Zafiropulo. On communicating finite-state machines. JACM, 30(2):323--342, 1983.
[15]
A. Bucchiarone, H. Melgratti, and F. Severoni. Testing service composition. In Proceedings of the 8th Argentine Symposium on Software Engineering (ASSE07), 2007.
[16]
G. Castagna, M. Dezani-Ciancaglini, and L. Padovani. On global types and multi-party session. LMCS, 8(1), 2012.
[17]
G. Cécé and A. Finkel. Verification of programs with half-duplex communication. I&C, 202(2):166--190, 2005.
[18]
W. W. W. Consortium. Web services choreography description language version 1.0. http://www.w3.org/TR/ws-cdl-10/, 2005.
[19]
J. Cortadella, M. Kishinevsky, L. Lavagno, and A. Yakovlev. Deriving Petri Nets for Finite Transition Systems. IEEE Trans. Computers, 47 (8):859--882, 1998.
[20]
P. Deniélou and N. Yoshida. Multiparty session types meet communicating automata. In ESOP, volume 7211 of LNCS, pages 194--213. Springer, 2012.
[21]
P.-M. Deniélou and N. Yoshida. Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types. In ICALP, volume 7966 of LNCS, pages 174--186, 2013.
[22]
M. Güdemann, G. Salaün, and M. Ouederni. Counterexample guided synthesis of monitors for realizability enforcement. In ATVA, volume 7561 of LNCS, pages 238--253, 2012.
[23]
S. Hallé and T. Bultan. Realizability analysis for message-based interactions using shared-state projections. In SIGSOFT FSE, pages 27--36. ACM, 2010.
[24]
K. Honda, N. Yoshida, and M. Carbone. Multiparty asynchronous session types. In POPL, pages 273--284. ACM, 2008.
[25]
J. Lange and E. Tuosto. Synthesising Choreographies from Local Session Types. In CONCUR, volume 7454 of LNCS, pages 225--239. Springer, 2012.
[26]
R. Lanotte, A. Maggiolo-Schettini, and A. Troina. Weak bisimulation for probabilistic timed automata. Theor. Comput. Sci., 411(50):4291--4322, 2010.
[27]
S. McIlvenna, M. Dumas, and M. T. Wynn. Synthesis of orchestrators from service choreographies. In APCCM, volume 96 of CRPIT, pages 129--138. ACS, 2009.
[28]
D. Mostrous, N. Yoshida, and K. Honda. Global principal typing in partially commutative asynchronous sessions. In ESOP, volume 5502 of LNCS, pages 316--332. Springer, 2009.
[29]
M. Mukund, K. N. Kumar, and M. A. Sohoni. Synthesizing distributed finite-state systems from MSCs. In CONCUR, volume 1877 of LNCS, pages 521--535. Springer, 2000.
[30]
A. Muscholl. Analysis of communicating automata. In LATA, volume 6031 of LNCS, pages 50--57. Springer, 2010.
[31]
G. Salaün, L. Bordeaux, and M. Schaerf. Describing and reasoning on web services using process algebra. In ICWS, pages 43--. IEEE Computer Society, 2004.
[32]
Y. Wang, A. Nazeem, and R. Swaminathan. On the optimal Petri net representation for service composition. In ICWS, pages 235--242. IEEE Computer Society, 2011.
[33]
D. M. Yellin and R. E. Strom. Protocol specifications and component adaptors. ACM Trans. Program. Lang. Syst., 19(2):292--333, 1997.

Cited By

View all
  • (2024)Safe Composition of Systems of Communicating Finite State MachinesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.414.3414(39-57)Online publication date: 11-Dec-2024
  • (2024)A simple view of multiparty session typesProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678252(1-3)Online publication date: 9-Sep-2024
  • (2024)Choral: Object-oriented Choreographic ProgrammingACM Transactions on Programming Languages and Systems10.1145/363239846:1(1-59)Online publication date: 16-Jan-2024
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
January 2015
716 pages
ISBN:9781450333009
DOI:10.1145/2676726
  • cover image ACM SIGPLAN Notices
    ACM SIGPLAN Notices  Volume 50, Issue 1
    POPL '15
    January 2015
    682 pages
    ISSN:0362-1340
    EISSN:1558-1160
    DOI:10.1145/2775051
    • Editor:
    • Andy Gill
    Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. choreography
  2. communicating finite-state machines
  3. global graphs
  4. multiparty session types
  5. theory of regions

Qualifiers

  • Research-article

Funding Sources

Conference

POPL '15
Sponsor:

Acceptance Rates

POPL '15 Paper Acceptance Rate 52 of 227 submissions, 23%;
Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)21
  • Downloads (Last 6 weeks)0
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Safe Composition of Systems of Communicating Finite State MachinesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.414.3414(39-57)Online publication date: 11-Dec-2024
  • (2024)A simple view of multiparty session typesProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678252(1-3)Online publication date: 9-Sep-2024
  • (2024)Choral: Object-oriented Choreographic ProgrammingACM Transactions on Programming Languages and Systems10.1145/363239846:1(1-59)Online publication date: 16-Jan-2024
  • (2024)Partially Typed Multiparty Sessions with Internal DelegationJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2024.101018(101018)Online publication date: Sep-2024
  • (2024)Team Automata: Overview and RoadmapCoordination Models and Languages10.1007/978-3-031-62697-5_10(161-198)Online publication date: 17-Jun-2024
  • (2024)Programming Language Implementations with Multiparty Session TypesActive Object Languages: Current Research Trends10.1007/978-3-031-51060-1_6(147-165)Online publication date: 29-Jan-2024
  • (2023)Partially Typed Multiparty SessionsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.383.2383(15-34)Online publication date: 21-Aug-2023
  • (2023)Communicating Actor Automata - Modelling Erlang Processes as Communicating MachinesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.378.4378(38-48)Online publication date: 13-Apr-2023
  • (2023)Multicompatibility for Multiparty-Session CompositionProceedings of the 25th International Symposium on Principles and Practice of Declarative Programming10.1145/3610612.3610614(1-15)Online publication date: 22-Oct-2023
  • (2023)Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint ProjectionProceedings of the ACM on Programming Languages10.1145/35860317:OOPSLA1(112-142)Online publication date: 6-Apr-2023
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media