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)