Safe Composition of Systems of Communicating Finite State Machines

TL;DR

This paper extends the Participants-as-Interfaces approach to the composition of multiple asynchronous communicating finite state machines, analyzing how connection policies affect the preservation of communication properties.

Contribution

It introduces a framework for multi-system composition with non-unique forwarding gateways and proves property preservation under certain connection policies.

Findings

Communication properties are preserved when connection policies satisfy certain conditions.

The approach generalizes binary composition to multiple systems.

Connection policies can be modeled as CFSM systems for analysis.

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.