Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Safe Composition of Systems of Communicating Finite State Machines

Franco Barbanera, Rolf Hennicker

TL;DR

The paper addresses safe multicomposition of asynchronous CFSM-based systems using the PaI paradigm. It introduces connection models and connection policies to govern dynamic forwarding between interfaces via gateways, enabling multi-system composition with configurable interaction patterns. The authors prove preservation of key communication properties—deadlock-freeness, orphan-message freeness, unspecified-reception freeness, and progress—under PaI multicomposition when both components and the connection policy satisfy the target property, noting necessary conditions like no-mixed-states for several properties and highlighting that lock-freeness is not generally preserved. The work demonstrates how structured connection policies enhance safe modular design and outlines directions for extending the framework to more complex interfacing infrastructures and stronger progress notions.

Abstract

The Participants-as-Interfaces (PaI) approach to system composition suggests that participants of a system may be viewed as interfaces. Given a set of systems,one participant per system is chosen to play the role of an interface. When systems are composed, the interface participants are replaced by gateways which communicate to each other by forwarding messages. The PaI-approach for systems of asynchronous communicating finite state machines (CFSMs) has been exploited in the literature for binary composition only, with a (necessarily) unique forwarding policy. In this paper we consider the case of multiple system composition when forwarding gateways are not uniquely determined and their interactions depend on specific connection policies complying with a connection model. We represent connection policies as CFSM systems and prove that a bunch of relevant communication properties (deadlock-freeness, reception-error-freeness, etc.) are preserved by PaI multicomposition, with the proviso that also the used connection policy does enjoy the communication property taken into account.

Safe Composition of Systems of Communicating Finite State Machines

TL;DR

The paper addresses safe multicomposition of asynchronous CFSM-based systems using the PaI paradigm. It introduces connection models and connection policies to govern dynamic forwarding between interfaces via gateways, enabling multi-system composition with configurable interaction patterns. The authors prove preservation of key communication properties—deadlock-freeness, orphan-message freeness, unspecified-reception freeness, and progress—under PaI multicomposition when both components and the connection policy satisfy the target property, noting necessary conditions like no-mixed-states for several properties and highlighting that lock-freeness is not generally preserved. The work demonstrates how structured connection policies enhance safe modular design and outlines directions for extending the framework to more complex interfacing infrastructures and stronger progress notions.

Abstract

The Participants-as-Interfaces (PaI) approach to system composition suggests that participants of a system may be viewed as interfaces. Given a set of systems,one participant per system is chosen to play the role of an interface. When systems are composed, the interface participants are replaced by gateways which communicate to each other by forwarding messages. The PaI-approach for systems of asynchronous communicating finite state machines (CFSMs) has been exploited in the literature for binary composition only, with a (necessarily) unique forwarding policy. In this paper we consider the case of multiple system composition when forwarding gateways are not uniquely determined and their interactions depend on specific connection policies complying with a connection model. We represent connection policies as CFSM systems and prove that a bunch of relevant communication properties (deadlock-freeness, reception-error-freeness, etc.) are preserved by PaI multicomposition, with the proviso that also the used connection policy does enjoy the communication property taken into account.

Paper Structure

This paper contains 6 sections, 2 theorems, 14 equations, 6 figures.

Table of Contents

  1. Introduction
  2. The PaI Approach to Multicomposition
  3. Systems of Communicating Finite State Machines
  4. PaI Multicomposition of Communicating Systems
  5. On the Preservation of Communication Properties
  6. Conclusions

Key Result

Theorem 5.1

Let $\{S_i\}_{i\in I}$ be a set of communicating systems composable with respect to a set $H = \{{ \mathtt{\color{blue}{ {h}}} }_i\}_{i \in I}$ of interfaces with no mixed states (cf. def:interfaces) and let $\mathbb{K}$ be a connection policy for $H$. Let $\mathcal{P}$ be either the property of d

Figures (6)

  • Figure 1: The PaI idea for binary composition
  • Figure 2: Four interface participants
  • Figure 3: Two possible choices of partners.
  • Figure 4: Two possible PaI multicompositions via gateways
  • Figure 5: The four communicating systems formalising the systems of Example \ref{['ex:simplewe']}
  • ...and 1 more figures

Theorems & Definitions (26)

  • Definition 3.1: CFSM
  • Definition 3.2: Communicating system and configuration
  • Definition 3.3: Reachable configuration
  • Definition 3.4: Communication properties
  • Example 4.1: Working example
  • Definition 4.2: Interfaces
  • Example 4.3
  • Definition 4.4: Connection model
  • Example 4.5: Some connection models
  • Definition 4.6: Local Connection Policy Set
  • ...and 16 more