BarbaneradLH19 (Article)
|
Author(s) | Franco Barbanera, Ugo de' Liguoro and Rolf Hennicker |
Title | « Connecting open systems of communicating finite state machines » |
Journal | J. Log. Algebr. Meth. Program. |
Volume | 109 |
Year | 2019 |
URL | https://doi.org/10.1016/j.jlamp.2019.07.004 |
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 CFSMs 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. |
Download the complete article:
@article{BarbaneradLH19,
volume = {109},
author = {Franco Barbanera and Ugo de' Liguoro and Rolf Hennicker},
url = {https://doi.org/10.1016/j.jlamp.2019.07.004},
localfile = {http://www.di.unito.it/~deligu/papers/JLAMP-2019b.pdf},
tag = {{J. Log. Algebr. Meth. Program.}},
title = {Connecting open systems of communicating finite state machines},
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 CFSMs 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.},
year = {2019},
doi = {10.1016/j.jlamp.2019.07.004},
journal = {J. Log. Algebr. Meth. Program.},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)