Global Types for Open Systems

TL;DR

This paper extends global-type formalisms to better describe open distributed systems, ensuring safety properties are maintained when such systems interact through compatible interfaces.

Contribution

It introduces interface roles and connections into global-type formalisms, enabling the modeling of open systems with preserved safety properties.

Findings

Safety properties are preserved when open systems are connected via compatible interfaces.

The extended formalism accurately models open systems of communicating finite state machines.

The approach facilitates safer composition of distributed systems.

Abstract

Global-type formalisms enable to describe the overall behaviour of distributed systems and at the same time to enforce safety properties for communications between system components. Our goal is that of amending a weakness of such formalisms: the difficulty in describing open systems, i.e. systems which can be connected and interact with other open systems. We parametrically extend, with the notion of interface role and interface connection, the syntax of global-type formalisms. Semantically, global types with interface roles denote open systems of communicating finite state machines connected by means of gateways obtained from compatible interfaces. We show that safety properties are preserved when open systems are connected that way.