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. © 2013 Elsevier B.V. All rights reserved.
Kokash, N., Jaghoori, M. M., & Arbab, F. (2013). From timed Reo networks to networks of timed automata. In Electronic Notes in Theoretical Computer Science (Vol. 295, pp. 11–29). https://doi.org/10.1016/j.entcs.2013.04.004