Communicating Finite State Machines (CFSMs) are an established model for describing and analysing distributed systems whose concurrently running components communicate via FIFO-channels. Systems of CESMs are usually considered as closed systems which do not provide access points for communication with the environment. In our study we relax this view such that certain components of a CFSM system can be looked at as describing the behaviour of the environment interacting with the system. They are considered as interfaces and if two systems posses compatible interfaces (according to a natural notion of compatibility) they can be connected. We propose a novel connection mechanism such that interface CFSMs are replaced by automatically generated "gateway" CFSMs, enabling messages to be exchanged between the systems. As a crucial outcome of our approach we prove that, under mild assumptions, if CFSM systems are connected in such a way a number of important communicating properties is preserved: deadlock-freeness, strong deadlock-freeness, orphan-message freeness, freeness of unspecified receptions, and progress. The communication properties we consider are those enjoyed by CFSM systems obtained by end-point projections of certain global type formalisms used in the field of asynchronous multiparty session types. To this end we introduce a parametric syntax to compose global types via interface roles. As a consequence of our preservation results we get for free that composed projected systems enjoy the communication properties. (C) 2019 Elsevier Inc. All rights reserved.
Connecting open systems of communicating finite state machines
Barbanera, Franco
Membro del Collaboration Group
;
2019-01-01
Abstract
Communicating Finite State Machines (CFSMs) are an established model for describing and analysing distributed systems whose concurrently running components communicate via FIFO-channels. Systems of CESMs are usually considered as closed systems which do not provide access points for communication with the environment. In our study we relax this view such that certain components of a CFSM system can be looked at as describing the behaviour of the environment interacting with the system. They are considered as interfaces and if two systems posses compatible interfaces (according to a natural notion of compatibility) they can be connected. We propose a novel connection mechanism such that interface CFSMs are replaced by automatically generated "gateway" CFSMs, enabling messages to be exchanged between the systems. As a crucial outcome of our approach we prove that, under mild assumptions, if CFSM systems are connected in such a way a number of important communicating properties is preserved: deadlock-freeness, strong deadlock-freeness, orphan-message freeness, freeness of unspecified receptions, and progress. The communication properties we consider are those enjoyed by CFSM systems obtained by end-point projections of certain global type formalisms used in the field of asynchronous multiparty session types. To this end we introduce a parametric syntax to compose global types via interface roles. As a consequence of our preservation results we get for free that composed projected systems enjoy the communication properties. (C) 2019 Elsevier Inc. All rights reserved.File | Dimensione | Formato | |
---|---|---|---|
communicating finite state machines.pdf
solo gestori archivio
Tipologia:
Versione Editoriale (PDF)
Licenza:
Creative commons
Dimensione
770.18 kB
Formato
Adobe PDF
|
770.18 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.