From timed Reo networks to networks of timed automata

Citations of this article
Mendeley users who have this article in their library.


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).

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free