Translating the Stochastic Reo Model of the ASK System into CTMC

Stochastic Reo and its semantic model

Stochastic Reo is an extension of Reo that supports reasoning about the quality of service (QoS) properties of service compositions. For this extension, we annotate Reo channels with delay rates and explicitly model data-arrival rates at the boundary nodes of a connector (see below), to capture its interaction with the services that comprise its environment.

For simplicity, we omit the node names in our circuits since they can be inferred from the names of their respective arrival rates: for instance, γa is the arrival rate of I/O requests at node a. From left to right, the channels are Sync, LossySync, SyncDrain, and FIFO1 channels.

Stochastic Reo Automata extend Reo automata to allow compositional derivation of a QoS-aware semantics of a Stochastic Reo circuit. The following table shows the Stochastic Reo Automata corresponding to the primitive Stochastic Reo channels shown above. Each automaton (left to right, top to bottom) corresponds to its respective channel (left to right) in the above figure.

The Stochastic Reo Automaton of a circuit is used as an intermediate model for translation from Stochastic Reo to a CTMC model.

ASK system

The ASK system is an industrial software that has been developed by Almende, and is marketed by ASK Community Systems. The ASK system provides the information or a service that matches the requirements of users in an efficient manner.

The top-level architecture of the ASK System is shown below. Every component in this architecture has its own internal architecture, with several levels of hierarchical nesting. At its top-level, the ASK system consists of three parts: web front-end, database, and contact engine as shown below. The web front-end deals with typical domain data such as user names, phone numbers, mail address, and so on. The database stores such typical domain data. The contact engine handles communication between the system and the outside world (e.g., by responding to or initiating telephone calls, sms, email, etc.) and provides appropriate matching and scheduling functionality.

A Reo model of the ASK System and its parts was developed by Almende in a case study within the EU project Credo for verification of its functional properties. We refined and augmented this Reo model with stochastic delays to derive a Stochastic Reo model for the ASK System. Together with Almende, we use this model to analyze and study the QoS properties of the ASK system in various settings. For instance, using Stochastic Reo Automata as an intermediate model, we can derive Continuous Time Markov Chain (CTMC) models from the Stochastic Reo model of the interesting parts of the ASK System, and feed them to CTMC analysis tools. It is not the intention of this introductory document to cover the entire model of the ASK System or its analysis. To illustrate our approach, we use here a very simple example of a generic task queue, which as one may expect, shows up frequently in all kinds of systems.

One main feature of the ASK system is the Request loop which means that incoming requests loop through the system repeatedly as various (sub-)tasks, until they are completely fulfilled. This Request loop is represented as a thick arrow in the figure above. Each component in the contact engine has a task/request queue that takes part in the realization of the Request loop. An arriving request that finds the queue full is dropped. The following figure shows the Stochastic Reo circuit for such a queue with the maximum capacity of 2:

The Stochastic Reo Automaton corresponding to this Stochastic Reo circuit is given below. In Stochastic Reo Automata, the nodes joined by synchronization disappear, but, to facilitate the understanding of the behavior of the queue, we keep the joined nodes in the labels of their respective firing transitions and highlight them in bold. An indexed Θ represents the composite delay information relevant for its respective firing transition.

Stochastic analysis

The CTMC model derived from the Stochastic Reo Automaton corresponding to the Stochastic Reo circuit of the task queue appears below. This figure shows the derived CTMC model in the textual format suitable as input to the PRISM tool for stochastic analysis.

We analyzed the derived CTMC model with the following simple but interesting properties of the queue:

This shows that the steady-state probability that the queue is more than 50% full (i.e., contains at least one task) is 0.438 when the task-arrival rate at the queue is twice the rate at which tasks are handled.

  • S=? [DataLost=MaxDataLost]

The above figure shows the variation of the steady-state probability that the queue loses new incoming tasks because it has no free capacity, as we keep the task arrival rate fixed and vary the task handling rate.

This example shows the analysis of the task queue with variable rates. If we put the actual arrival and service rates of a real deployed system in this derived CTMC model, then we can determine, e.g., whether or not the number of available server components are sufficient to deal with the tasks for efficient and reasonable processing in the actual system.

In this case study, we briefly showed an example of our approach to the translation from Stochastic Reo into CTMC via Stochastic Reo automata. For a more detailed explanation of this approach see the technical report A Compositional Semantics for Stochastic Reo Connectors. Currently, the implementation of the tools for this approach and their application to the full model of the ASK system is under way.