Introduction
Few new technologies have been embraced with as much enthusiasm as cloud
computing. Users, providers and policy makers have set out to exploit the
advantages of the new technology and to encourage its adoption. Their success
stories abound, and the range of services delivered by cloud-based systems is
growing at a fast pace. Business-critical e-commerce and e-government services,
and safety-critical healthcare services are increasingly part of this range.
Using cloud-based systems to deliver critical services is a double-edged sword.
On the one hand, the ability of cloud to dynamically scale resource allocations in
line with changing workloads makes it particularly suited for running such
systems. On the other hand, its reliance on third-party hardware, software and
networking can lead to violations of the strict non-functional requirements (NFRs)
associated with critical services. Taking advantage of the former characteristic of
cloud without being adversely a ected by the latter represents a great challenge,
as the traditional approaches to verifying NFRs are often ine ective in a cloud
setting. NFR veri cation approaches such as model checking, design by contract
and quality assurance were devised for o -line use during the design or veri
cation and validation stages of system development. As a result, they have high
overheads and operate with models and non-functional properties (NFPs) that
in the case of cloud-based systems evolve continually as the workloads, allocated
resources and requirements of these systems change over time.
In this survey paper, we describe how a formal technique called runtime
quantitative veri cation [
1
] can be used (a) to verify the NFPs of evolving
cloudbased systems continually; and (b) to guide this evolution towards con gurations
that are guaranteed to satisfy the system NFRs.
This work was partly supported by the UK EPSRC grant EP/H042644/1.
Runtime Quantitative Veri cation
Quantitative veri cation is a mathematically based technique for analysing the
correctness, performance and reliability NFPs of systems that exhibit stochastic
behaviour [
14
]. To analyse the NFPs of a system, the technique uses nite-state
Markov models comprising states that correspond to di erent system con
gurations, and edges associated with the transitions that are possible between
these states. Depending on the type of the analysed NFPs, the edges are
annotated with transition probabilities or transition rates; and the model states
and transitions may additionally be labelled with costs/rewards. Given a model
and an NFP speci ed formally in temporal logic extended with probabilities
and costs/rewards, probabilistic model checkers that implement the technique
analyse the model exhaustively in order to evaluate the property.
Like most formal veri cation techniques, quantitative veri cation is
traditionally used in o -line settings, to evaluate the performance-cost tradeo s of
alternative system designs, or to analyse NFR compliance for existing systems. In
the latter case, systems in violation of their NFRs undergo o -line maintenance.
This approach does not meet the demands of emerging application scenarios
in which systems need to be continually veri ed as they adapt autonomously,
whenever a need for change is detected while they operate [
6
]. To address this
need for continual veri cation, the runtime variant of the approach depicted in
Fig. 1 was introduced in [
10, 11
] and further re ned in [
1, 4, 9, 12
].
family of system
models for
different scenarios
model
selection
system & environ.
parameters defining
the current scenario
monitor system
& its environment
cloud-based
system
selected
model
reconfiguration
plan
non-functional
requirements
quantitative
verification
quantitative
verification
results
verification result
analysis & new
config. selection
Continual Veri cation of Cloud-Deployed Services
Continual veri cation can be used to manage the reliability of multi-tier software
services deployed on cloud infrastructure owned by the service provider. As we
show in [
8, 13
], quantitative veri cation at runtime enables service administrators
to quantify the impact of planned and unexpected changes on the reliability of
their services, as the approach provides precise answers to questions such as:
Q1 What is the maximum probability of a service becoming unavailable within
a one-month time period?
Q2 How will the probability of failure for a service be a ected if one of its
database instances is switched o to re ect a decrease in service workload?
Q3 How many additional VMs should be used to run a service component when
moving it to VMs placed on servers with fewer memory blocks?
Service administrators (or their automated resource management scripts) can
then respond with remedial action if the service fails to comply with its NFRs,
e.g., by discarding the planned removal of a component instance.
Compositional NFR Veri cation Standard veri cation uses a monolithic
model constructed from the parallel composition of models of all system
components, in order to capture interleaving and synchronised behaviour between
components. Despite signi cant improvements in the e ciency of quantitative
veri cation techniques and tools, this often results in high overheads that make
the runtime use of the technique unfeasible because the system may change again
before its latest change has been fully analysed. This problem is addressed by
compositional NFR veri cation, a formal technique that replaces the analysis
of monolithic system models with a sequence of veri cation steps carried out
component-wise on local NFPs. The ordering of the steps is determined
according to component dependencies within the analysed system, and ultimately helps
infer global system NFPs. Compositional veri cation reduces the NFP analysis
overheads signi cantly, and in [
8
] we show that it can be used for continual NFP
veri cation in certain scenarios associated with cloud-based systems.
Incremental NFR Veri cation Cloud-deployed services operate in a highly
dynamic environment where service components are frequently added, removed
and scaled according to demand, or might fail unexpectedly. While
compositional veri cation broadens the range of systems to which NFR veri cation can
be applied e ectively, it cannot cope with such rapid changes. Our INVEST
incremental veri cation framework from [
13
] addresses this limitation by
identifying and executing a minimal sequence of reveri cation steps after each change
in a component-based system.
Practical Use Using our continual NFR veri cation of cloud-deployed
services requires the construction of accurate models of the analysed system and
the speci cation of its NFRs in probabilistic temporal logic. As most
practitioners lack the formal methods expertise required to carry out this task, we
developed domain-speci c languages that administrators of cloud resources can
use to specify the initial structure of their multi-tier cloud-deployed services and
the changes under which their NFPs should be analysed [
16
].
Continual Veri cation of Service-Based Systems
Continual NFP veri cation can also be exploited by cloud-service users, to drive
the dynamic selection of service-based system (SBS) components. Built through
the integration of third-party services deployed on cloud datacentres and
accessed over the Internet, SBSs are increasingly used in business-critical and
safety-critical applications in which they must comply with strict NFRs.
Selfadaptive SBSs achieve NFR compliance by selecting the concrete services for
their operations dynamically, from sets of functionally equivalent third-party
services with di erent levels of performance, reliability and cost.
Continually veri ed SBSs The self-adaptive SBS architecture and
development methodology we introduced in [
2
] and extended in [
1, 7
] carry out this
concrete service selection using continual NFR veri cation. Given an SBS
workow comprising n 1 operations to be performed by third-party services, our
SBS architecture uses intelligent proxies to interface the work ow with sets of
remote service such that the i -th SBS operation can be carried out by mi > 1
functionally equivalent services. The main role of the intelligent proxies is to
ensure that each execution of an SBS operation is carried out through the
invocation of a concrete service selected as described below. The proxy overseeing
the i -th SBS operation is initialised with a sequence of \promised" service-level
agreements slaij = (pi0j ; cij ); 1 6 j 6 mi , where pi0j 2 [0; 1] and ci;j > 0 represent
the provider-supplied probability of success and the cost for an invocation of
service si;j , respectively. The intelligent proxies are also responsible for
notifying a model updater about each service invocation and its outcome. The model
updater starts from a developer-supplied initial Markov model of the SBS
workow, and uses the on-line learning techniques from [
3, 5
] to adjust the transition
probabilities of the model in line with these proxy noti cations. Finally, the
upto-date Markov model is used by an autonomic manager that performs runtime
quantitative veri cation to select the service combination used by the intelligent
proxies so that the SBS satis es its NFRs with minimal cost at all times.
E cient NFR Veri cation The runtime quantitative veri cation within
our framework [
3, 5
] is carried out by an embedded version of the PRISM
probabilistic model checker [
15
]. This version of PRISM can handle the \on the y"
analysis necessary for a range of small-sized SBS work ows. The compositional
and incremental veri cation approaches described in the previous section can be
used to reduce the overheads of continual NFP veri cation in order to extend
its applicability to larger SBS work ows.
Practical Use For a continually veri ed SBS architecture to be practical,
developers should be able to build instances of it without requiring special training
in formal methods. To address this need, our work from [
3, 5
] introduced a
toolsupported SBS development framework. In this framework, many of the
components and artefacts described above are either generated automatically (e.g.,
starting from an annotated UML activity diagram of the SBS work ow and from
the WSDL speci cations of its concrete services) or work ow-independent and
therefore provided as reusable middleware.
A key advantage of cloud-based systems is their ability to evolve, e.g., by
scaling their resources up and down in response to changes in workload. When
such evolving systems deliver business-critical or safety-critical services, their
non-functional properties (NFPs) must be veri ed continually. We summarised
recent research into using quantitative model checking to support continual NFP
veri cation in cloud-based systems. This novel approach to NFP veri cation can
be exploited by both providers and users of cloud-deployed services, and has been
employed successfully in several case studies, e.g. [
1, 5, 7, 8, 13
]. Nevertheless,
signi cant research is still needed to extend its applicability to new scenarios, to
improve its scalability, and to identify and address its limitations.