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 9788793519824. (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)

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: Faculties > Sciences > School of Computing
Depositing User: Julien Lange
Date Deposited: 20 Jul 2017 16:25 UTC
Last Modified: 20 Jul 2017 16:25 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/62371 (The current URI for this page, for reference purposes)
Lange, Julien: https://orcid.org/0000-0001-9697-1378
  • Depositors only (login required):