skip to main content
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
  • (2023)Composition of synchronous communicating systemsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2023.100890135(100890)Online publication date: Oct-2023
  • (2023)Event structure semantics for multiparty sessionsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2022.100844131(100844)Online publication date: Feb-2023
  • (2022)Composable partial multiparty session types for open systemsSoftware and Systems Modeling10.1007/s10270-022-01040-x22:2(473-494)Online publication date: 28-Sep-2022
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

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
  • 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
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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015
Published in SIGPLAN Volume 50, Issue 1

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

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

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

Other Metrics

Citations

Cited By

View all
  • (2023)Composition of synchronous communicating systemsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2023.100890135(100890)Online publication date: Oct-2023
  • (2023)Event structure semantics for multiparty sessionsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2022.100844131(100844)Online publication date: Feb-2023
  • (2022)Composable partial multiparty session types for open systemsSoftware and Systems Modeling10.1007/s10270-022-01040-x22:2(473-494)Online publication date: 28-Sep-2022
  • (2022)ST4MP: A Blueprint of Multiparty Session Typing for Multilingual ProgrammingLeveraging Applications of Formal Methods, Verification and Validation. Verification Principles10.1007/978-3-031-19849-6_26(460-478)Online publication date: 17-Oct-2022
  • (2021)Assuming just enough fairness to make session types complete for lock-freedomProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470531(1-13)Online publication date: 29-Jun-2021
  • (2021)Composable Partial Multiparty Session TypesFormal Aspects of Component Software10.1007/978-3-030-90636-8_3(44-62)Online publication date: 28-Oct-2021
  • (2020)Composing Communicating Systems, SynchronouslyLeveraging Applications of Formal Methods, Verification and Validation: Verification Principles10.1007/978-3-030-61362-4_3(39-59)Online publication date: 29-Oct-2020
  • (2020)On Testing Message-Passing ComponentsLeveraging Applications of Formal Methods, Verification and Validation: Verification Principles10.1007/978-3-030-61362-4_2(22-38)Online publication date: 29-Oct-2020
  • (2020)A Choreography-Driven Approach to APIs: The OpenDXL Case StudyCoordination Models and Languages10.1007/978-3-030-50029-0_7(107-124)Online publication date: 10-Jun-2020
  • (2020)Choreography AutomataCoordination Models and Languages10.1007/978-3-030-50029-0_6(86-106)Online publication date: 10-Jun-2020
  • 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