Translation of Stochastic Reo into CTMC in ASK system

Stochastic Reo and its semantic model

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

For simplicity, the node names are omitted since they can be inferred from the names of their respective arrival rates: for instance, γa is the arrival rate of node a. From the left, each channel is Sync, LossySync, SyncDrain, and FIFO1 channels.

Stochastic Reo automata, as an extension of Reo automata, compositionally derive a QoS-aware semantics for Stochastic Reo. The following table shows Stochastic Reo Automata corresponding to primitive Stochastic Reo channels shown above, each automaton of which corresponds to the channel from left to right in a row.

Such a Stochastic Reo automaton is used as an intermediate model for the translation from Stochastic Reo to a CTMC model.

ASK system

The ASK system is an industrial software that has been developed by Almende, which is marketed by ASK Community Systems. The ASK system provides information or a service that matches the requirement of users in the efficient way. The ASK system consists of three parts: web front-end, database, and contact engine as shown below. The web front-end acts as a typical domain data such as users, 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 and provides appropriate matching and scheduling functionality.

The main feature of the ASK system is the Request loop which means that requests loop through the system until they are completely fulfilled. Such a Request loop is described in a thick arrow above. Here, we concern a task/request queue in each component in the contact engine, which plays an important role for the Request loop. We designed a task/request queue as:

It can stores at most two tasks, thereafter further coming tasks are lost until one of the two tasks in the buffers is consumed by the outside (in this case, a certain component handles the tasks).

The Stochastic Reo automaton corresponding to this Stochastic Reo model for the queue is given below. In Stochastic Reo automata, the joined nodes by synchronization are not depicted, but, for easy understanding the behavior of the queue, we keep the joined nodes in the labels on their relevant firing transitions, which appear in bold. The indexed Θ represents the delay rates relevant to its firing transitions.

Stochastic analysis

We derived the CTMC model from corresponding to the Stochastic Reo automaton shown above. The following figure shows that the textual format of the derived CTMC model is fed to PRISM for stochastic analysis.

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

It shows that the steady-state probability of the queue is more than 50% full when the task-arrival at the queue is twice frequent than the handling tasks.

  • S=? [DataLost=MaxDataLost]

It shows the change of the steady-state probability of that the queue loses coming data because of the lack of its capacity. In this example, we showed the analysis on the task queue with arbitrary rates. With the derived CTMC model having actual rates, then we can figure out how many components are required to deal with the tasks for efficient and reasonable processing in the actual ASK system.