Correlating Formal Semantic Models of Reo Connectors: Connector Coloring and Constraint Automata

TL;DR

This paper investigates the relationship between two key semantic models of Reo connectors, defining transformations and proving their correctness to enhance understanding and tool applicability.

Contribution

It introduces operators for transforming coloring models and constraint automata, proving their correctness and compositionality, and extends coloring models with data constraints.

Findings

Operators for model transformation are correct and compositional.

Coloring models and constraint automata are shown to be equivalent.

Transformations enable broader tool applicability for Reo connectors.

Abstract

Over the past decades, coordination languages have emerged for the specification and implementation of interaction protocols for communicating software components. This class of languages includes Reo, a platform for compositional construction of connectors. In recent years, various formalisms for describing the behavior of Reo connectors have come to existence, each of them serving its own purpose. Naturally, questions about how these models relate to each other arise. From a theoretical point of view, answers to these questions provide us with better insight into the fundamentals of Reo, while from a more practical perspective, these answers broaden the applicability of Reo's development tools. In this paper, we address one of these questions: we investigate the equivalence between coloring models and constraint automata, the two most dominant and practically relevant semantic models of Reo. More specifically, we define operators that transform one model to the other (and vice versa), prove their correctness, and show that they distribute over composition. To ensure that the transformation operators map one-to-one (instead of many-to-one), we extend coloring models with data constraints. Though primarily a theoretical contribution, we sketch some potential applications of our results: the broadening of the applicability of existing tools for connector verification and animation.