Skip to main content
Kent Academic Repository

A Tool for Choreography-Based Analysis of Message-Passing Software

Lange, Julien and Tuosto, Emilio and Yoshida, Nobuko (2017) A Tool for Choreography-Based Analysis of Message-Passing Software. In: Behavioural Types: from Theory to Tools. River Publishers. ISBN 978-87-93519-82-4. (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided) (KAR id:62371)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided. (Contact us about this Publication)
Official URL:
http://www.riverpublishers.com/pdf/ebook/chapter/R...

Abstract

An appealing characteristic of choreographies is that they provide two complementary

views of communicating software: the global and the local views. Communicating finite-state machines (CFSMs) have been proposed as an expressive formalism to specify local views. Global views have been represented

with global graphs, that is graphical choreographies (akin to BPMN and UML) suitable to represent general multiparty session specifications. Global graphs feature expressive constructs such as forking, merging, and

joining for representing application-level protocols. An algorithm for the reconstruction of global graphs from CFSMs has

been introduced in [17]; the algorithm ensures that the reconstructed global graph faithfully represents the original CFSMs provided that they satisfy a suitable condition, called generalised multiparty compatibility (GMC). The

CFSMs enjoying GMC are guaranteed to interact without deadlocks and other communication errors. After reviewing the basic concepts underlying global graphs, communicating machines and safe communications, we highlight the main features of ChorGram, a tool implementing the generalised multiparty compatibility and reconstruction of global graphs of [17]. We

overview the architecture of ChorGram and present a comprehensive example to illustrate how it is used directly to analyse message-passing software and programs.

Item Type: Book section
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Julien Lange
Date Deposited: 20 Jul 2017 16:25 UTC
Last Modified: 16 Feb 2021 13:46 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/62371 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.