Database of Research Tools Developed Using CADP


Organisation: Universidade do Minho Praga (PORTUGAL)
Radbouud University Nijmegen (THE NETHERLANDS)

Functionality: Translation from Reo to IMC

Tools used: CADP (Construction and Analysis of Distributed Processes)

Period: 2014.

Description: Channel based-languages play a prominent role in the world of software composition. One of such languages is Reo, where complex connectors are constructed by composing various types of primitive channels. Stochastic Reo is an extension of Reo, allowing the specification of stochastic values for the channels (e.g., arrival and processing rates). Having stochastic values enables to analyze the quality of service for composed software (intensive) systems, with the goal of evaluating and improving performance and resource allocation in service-oriented applications.

Using interactive Markov chains (IMC) as a semantic model for stochastic Reo, it is possible to obtain models satisfying many desired properties, including context dependency (where a behaviour might depend upon both the presence and absence of I/O requests on the boundary ports of the connector) and compositionality (which enables a powerful analysis of complex systems). Furthermore, the obtained models can be analysed using existing tools such as CADP.

This appraochn is supported by a tool chain, divided into two main parts: one for building the model from the composition of several Reo channels, and another one for its analysis. The first component (to which we refer to as IMCREOtools) takes as input a description of a Reo connector with stochastic information based on the CooPLa language. It composes a (randomly selected) initial channel with the subsequent ones, applying techniques to limit state space explosion and improve composition efficiency. This creates an IMC Reo, which is then linearly converted into a standard IMC. The second component resorts to tools like CADP for the quantitative and qualitative analysis of the generated IMC.

Conclusions: The modelling of stochastic Reo with IMC enables, without significant effort, the use of the interesting and powerful means to analyse and model check IMC provided by CADP.

Publications: [Oliveira-Silva-Barbosa-14] Nuno Oliveira and Alexandra Silva and Luís S. Barbosa. "Quantitative Analysis of Reo-based Service Coordination". Proceedings of the 29th Symposium on Applied Computing SAC 2014, pp. 1247-1254, ACM, March, 2014.
Available on-line at:
or from the CADP Web site in PDF or PostScript

[Moon-Silva-Krause-Arbab-14] Y-J. Moon, A. Silva, Ch. Krause, and Farhad Arbab. "A Compositional Model to Reason about End-to-End QoS in Stochastic Reo Connectors". Science of Computer Programming 80(A):3-24, 2014.
Available on-line at:
or from the CADP Web site in PDF or PostScript

[Oliveira-Silva-Barbosa-15] Nuno Oliveira and Alexandra Silva and Luís S. Barbosa. "IMCReo: Interactive Markov Chains for Stochastic Reo". Journal of Internet Services and Information Security 5(1):3-28, 2015.
Available on-line at:
or from the CADP Web site in PDF or PostScript

Alexandra Silva
Department of Computer Science
University College London
Gower Street
London WC1E 6BT
Phone: +44 (0) 20 7679 0319

Further remarks: This tool, amongst others, is described on the CADP Web site:

Last modified: Thu Feb 11 12:23:11 2021.

Back to the CADP research tools page