Modeling real-time coordination systems using timed Büchi automata

Reo is an exogenous coordination language for synthesizing components participating in a component-based system. The notion of Büchi automaton over streams of records (BAR for short) is a proposed operational semantics for Reo that covers several aspects of coordination strategies such as synchronization, context dependencies and fairness constraints. In this paper and for the purpose of modeling real-time coordination systems specified by Reo, we present a timed version of BARs as the acceptors of timed streams of records. We show that timed BAR and its streams of records based semantics are more standard and also more expressive than timed constraint automaton which is the first proposed operational model of timed Reo connectors.