IMC_Reo: interactive Markov chains for Stochastic Reo

Nuno Oliveira¹⁺, Alexandra Silva², and Luís S. Barbosa¹

¹HASLab INESC TEC, Universidade do Minho, Braga, Portugal
{nuno.s.oliveira, luis.s.barbosa}@insectec.pt

²Centrum Wiskunde & Informatica, Radboud University Nijmegen, Nijmegen, the Netherlands

alexandra@cs.ru.nl

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.

Keywords: Interactive Markov chains, Stochastic analysis, Coordination, Reo

+: Corresponding author: Nuno Oliveira
Departamento do Informatica, Universidade do Minho, Campus de Gualtar, Braga 4710-057, Portugal,

Tel: +351-253-604-470, Web: http://alfa.di.uminho.pt/~nunooliveira

Journal of Internet Services and Information Security (JISIS), 5(1): 3-28, February 2015 [pdf]