From Timed Reo Networks to Networks of Timed Automata

The Reo coordination language is an extensible graphical notation for component or service coordination wherein independent autonomous software entities exchange data through a connector or a network imposing synchronization and data constraints on those entities. Each connector is formed from a set of binary connectors, called channels, with precise semantics and, thus, amenable to formal verification. However, the development of verification tools for Reo-specific semantic models, namely, constraint automata with its multiple extensions to represent quality of service, time constraints, context-dependent or probabilistic behavior would require years of research and development. A much more promising approach is to exploit already existing verification tools. In this paper, we present a mapping of timed Reo networks to networks of timed automata used for system specification in Uppaal. Uppaal is a state-of-the-art toolset for modeling, validation and verification of real-time systems used in many large-scale industrial projects. Our work enables its application to the compositional analysis of timed service-based workflow models specified with Reo.