Safe message forwarding preserves communication properties in composed systems
Safe Composition of CFSM Systems via Partial Gateways
Logic in Computer Science
Summary
When combining multiple communicating systems, one challenge is ensuring they work correctly without problems like deadlocks or message errors. The authors show a way to connect parts of these systems using special components called partial gateways that only forward selected messages. They prove that if the original systems and the connection policy are safe, then the composed system also remains safe. This finding helps build larger systems by safely linking smaller ones through controlled message forwarding.
What this means in practice
- •For distributed system engineers: Ensure safe integration of communicating components by using partial gateways that forward selected messages while preserving key communication properties.
- •For protocol developers: Design protocol compositions that avoid deadlocks and errors by applying fusion-composition based methods to control message interactions between components.
A theory result. No direct application yet.
Authors
Franco Barbanera
Abstract
The Participants-as-Interfaces (PaI) methodology for system composition proposes that system participants can be regarded as interfaces. For each system in a given collection, one participant is designated to serve as its interface. When the systems are composed, these interface participants are replaced with gateways that communicate with one another by forwarding messages. We generalise the approach to partial gateways, where gateways can forward only a chosen set of messages. As for the standard PaI approach, we exploit such extended version for systems of communicating finite state machines (CFSMs). This extension is fully detailed for the binary case, and can be scaled up to the multicomposition case. We prove that many relevant communication properties (deadlock-freeness, reception-error-freeness, etc.) are preserved by PaI composition via partial gateways in case also the connection policy (i.e. the system representing the way we wish gateways interact with each other) enjoys the same properties. Such a proof turns out to be just a corollary of a property preservation result for a restricted and partial composition method, dubbed fusion-composition. Fusion-composition hence turns out to be at the heart of the PaI composition approach.