Application Domains
Domain 1: ePMC of Service-Based Systems
Overview
Service-based systems (SBSs) enable the effective development of new applications through the integration of third-party and in-house components implemented as services. There are many ways in which services can perform the same SBS operation and each may have different probabilities of success p1,p2,... costs c1,c2,... and execution times t1,t2,...
We consider 8 different modelling patterns for the implementation of SBS operations using n functionally-equivalent services
Modelling patterns for the implementation of SBS operations.
To demonstrate ePMC in the SBS doman we consider a six-component service-based foreign exchange system first introduced by Gerasimou et al. Traders can use the FX system in “normal” or “expert” operation modes. In its normal mode, the system uses a Fundamental Analysis component to decide whether a transaction should be performed, or the fundamental analysis should be retried, or the normal-mode session should be ended. Performing a transaction involves using an Order component to carry out the operation, and is followed by the invocation of a Notification component to inform the trader about the outcome of the transaction. In its expert mode, the system uses a Market Watch component to obtain exchange market data that is then processed by a Technical Analysis component. The result of this analysis may satisfy a set of trader-specified objectives (in which case a transaction is performed), may not meet these objectives (so the Market Watch is reinvoked for an update) or may be erroneous (in which case an Alarm component is used to warn the trader). In our experiments, we assumed that the probabilities that annotate the decision points from the diagram in Fig. 7 (i.e., the operational profile of the FX system) were unknown parameters x, y1, y2, z1 and z2.
Foreign exchange system from the SBS domain
Evaluation
We considered multiple ways in which the six FX components could be implemented using the SBS modelling patterns with between one and five functionally-equivalent services per component. We then considered three QoS properties of the systems.
- P1 The probability of successful completion;
- P2 The expected execution time;
- P3 The expected cost.
The table below shows that the PMC time required to analyse the three properties using ePMC is always better, and typically orders of magnitude smaller, than the PMC times of PRISM, Storm and PARAM (except for the trivial case when a single service is used for each SBS component, cf. row 1). Moreover, the three tools ran out of memory or timed out when components used four (and sometimes even two or three) services, with the exception of the Storm analyses of the PROB pattern, which were all completed. The reason for this is that PROB is by far the SBS modelling pattern with the simplest QoS-property expressions, i.e., just linear combinations of the service parameters. Note also that ePMC analysis times are almost identical irrespective of the property analysed and of the pattern and number of services used. This is because the time required to run our ePMC tool is dominated by the time used to read the files containing the ePMC repository of QoS-property expressions and the annotated MC, to start Storm and to parse the MC, all of which do not depend on the analysed property or the patterns from the model annotations.
The last row from Table 9 reports the minimum, maximum and mean PMC time and the standard deviation over 20 experiments in which the pattern and number of services (two or three) used for each component were chosen randomly and independently of those of the other components. We only used the patterns SEQ, PAR and PROB in these experiments so that at least Storm could complete the analysis, albeit with PMC times much longer than ePMC; PRISM and PARAM timed out in all 20 experiments.
Parametric model checking time (seconds) for the FX SBS.
ePMC repository, models and properties
| File | Description |
|---|---|
| Repository of QoS-property expressions | ePMC repository containing the modelling patterns for the SBS domain. |
| Monolithic Markov models | ZIP file containing the monolithic models for analysis in PRISM/Storm and PARAM format |
| Pattern-annotated Markov model | Pattern-annotated Markov model (with an annotation example) for analysis in ePMC. |
| Analysed PCTL properties | Analysed PCTL properties |
Domain 2: ePMC of Multi-Tier Architectures
Overview
As a second application domain for ePMC, we consider the deployment of software systems with a multi-tier architecture on a set of servers. For improved reliability and throughput, these systems often use horizonal distribution within some or all tiers, i.e. they have instances of these tiers running on multiple servers. We devised a repository of server modelling patterns for analysing reliability properties of such systems. To this end, we consider different types of server on which n1 ≥ 1, n2 ≥ 1, ... , nm ≥ 1 instances of m of the system tiers were deployed.
A non-exhaustive set of server modelling patterns was then devised as shown in the table below.
Modelling patterns for the implementation of Multi-Tier Architecture operations.
The BASIC pattern from this table corresponds to a server whose failure leads to the immediate loss of all tier instances running on the server, while the VIRTUALIZED and VIRTUALIZED-M(onitored) patterns correspond to servers where each instance of a tier is running within a separate virtual machine (VM). The difference between the two types of virtualized server is that the second type has a monitor component capable of detecting imminent server failures early enough to allow the migration of the VMs to other servers.
Evaluation
We assume that the engineers responsible for deploying a multi-tier software system on a combination of such servers need to assess the following reliability properties of alternative deployment options:
- PFAIL The probability of system failure due to all in- stances of a tier failing within a time period of interest;
- PSPF The probability of a single point of failure (i.e. a tier with a single operational instance) occurring within the analysed time period.
We evaluated ePMC within this domain by using it to analyse the properties PFAIL and PSPF for eight four-server deployments of a three-tier system. The characteristics of these deployments and the time taken by the parametric model checking of the two properties are shown in the table below.
Parametric model checking time (seconds) for the FX SBS.
As for the SBS domain, the ePMC model checking time is largely unaffected by the system size, remaining under 1s when the total number of tier instances increases from six instances for deployments D1 and D2 to 40 instances for deployments D7 and D8. In contrast, the model checking time for PRISM, Storm and PARAM increases rapidly with the system size. As D1, D3, D5 and D7 use only the simpler, loop-free deployment patterns BASIC and VIRTUALIZED, the three model checkers can successfully analyse deployments D1, D3 and D5. However, the analysis times of these tools are already orders of magnitude larger than those of ePMC for the larger deployment D5 (and their analyses of deployment D7 time out). The better efficiency of ePMC is even clearer for deployments D2, D4, D6 and D8, which use the more complex deployment pattern VIRTUALIZED-M: out of these deployments, only D2 can be successfully analysed by PRISM, Storm and PARAM.
ePMC repository, models and properties
| File | Description |
|---|---|
| Repository of QoS-property expressions | ePMC repository containing the modelling patterns for the multi-tier architecture domain |
| Monolithic Markov models | ZIP file containing the monolithic models for analysis in PRISM/Storm and PARAM format |
| Pattern-annotated Markov models | Pattern-annotated Markov models for analysis in ePMC |
| Analysed PCTL properties | Analysed PCTL properties |