We present an operational semantics for a component composition language called Reo. Reo connectors exogenously compose and coordinate the interactions among individual components that comprise a complex system, into a coherent collaboration. The formal semantics we present here paves the way for a rigorous study of the behavior of component composition mechanisms. To demonstrate the feasibility of such a rigorous approach, we give a faithful translation of Reo semantics into the Maude term rewriting language. This translation allows us to exploit the rewriting engine and the model-checking module in the Maude tool-set to symbolically run and model-check the behavior of Reo connectors.
(Paper in .ps format in .pdf format) (Presentation in .pdf format)
A detailed version of this paper has appeared as:
M.R. Mousavi, M. Sirjani, F. Arbab, Specification, Simulation, and Verification of Component Connectors in Reo, Technical Report CSR-04-15, Department of Computer Science, Eindhoven University of Technology, Eindhoven, The Netherlands, June 2004.
(Technical Report in .ps format in .pdf format)
Accompanying Maude code in .tgz format . (updated August 2007)
@InProceedings{MousaviFoclasa05,
title = "Formal Semantics and Analysis of Component Connectors in {R}eo",
author = "Mousavi, MohammadReza and Sirjani, Marjan and Arbab, Farhad",
booktitle = "Proceedings of the 4th International Workshop on the
Foundations of Coordination Languages and Software Architectures (FOCLASA'05)",
series = "Electronic Notes in Theoretical Computer Science",
year = "2005",
note = "To appear"
}