Volume 5 - Issue 1
IMCReo: interactive Markov chains for Stochastic Reo
- Nuno Oliveira
HASLab INESC TEC, Universidade do Minho, Braga, Portugal
nuno.s.oliveira@insectec.pt
- Alexandra Silva
Centrum Wiskunde & Informatica, Radboud University Nijmegen, Nijmegen, the Netherlands
alexandra@cs.ru.nl
- Luıs S. Barbosa
HASLab INESC TEC, Universidade do Minho, Braga, Portugal
luis.s.barbosa@insectec.pt
Keywords: Interactive Markov chains, Stochastic analysis, Coordination, Reo
Abstract
The study of composed software and its properties is in itself a great challenge. Bringing quantitative
aspects into the picture increases the complexity of the analysis and entails the need for reconciling
both the classical and the stochastic analyses. The quest herein is to provide constructs for composition
of building blocks and semantic models thereof which enable both analyses and allow for
modeling and verification. Stochastic Reo offers constructs for component and service coordination
and provides means for specification of stochastic values for software connectors. Interactive
Markov chains (IMC) on the other hand, are a stochastic, compositional, extension of classical models
of concurrency, integrating classical and stochastic aspects. This paper discusses how IMC can
be effectively used as a compositional semantic model for Stochastic Reo, avoiding to resort to
a separate automaton model, often lacking full compositionality, as intermediate semantics. A tool
chain integrating available tool support for IMC, is described and applied in the analysis of a case
study dealing with performance and resource allocation of a mediation system.