Handshaking Protocol for Distributed Implementation of Reo

TL;DR

This paper introduces a formal implementation model for distributed Reo, incorporating communication delays, and proposes Timed Action Constraint Automata to verify correctness of handshaking protocols in service coordination.

Contribution

It presents a novel formal model for distributed Reo with delays and introduces TACA for reasoning about its correctness.

Findings

TACA effectively models handshaking behavior in Reo.

Distributed Reo implementation can be verified using TACA.

The approach supports reasoning about communication delays in service coordination.

Abstract

Reo, an exogenous channel-based coordination language, is a model for service coordination wherein services communicate through connectors formed by joining binary communication channels. In order to establish transactional communication among services as prescribed by connector semantics, distributed ports exchange handshaking messages signalling which parties are ready to provide or consume data. In this paper, we present a formal implementation model for distributed Reo with communication delays and outline ideas for its proof of correctness. To reason about Reo implementation formally, we introduce Timed Action Constraint Automata (TACA) and explain how to compare TACA with existing automata-based semantics for Reo. We use TACA to describe handshaking behavior of Reo modeling primitives and argue that in any distributed circuit remote Reo nodes and channels exposing such behavior commit to perform transitions envisaged by the network semantics.