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

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.