Initially, the cloud deployed system comprises
- four servers serverA,serverB,serverC and serverD.
- serverA hosts two VM's: one running web and the other app
(webappA)
- serverB hosts two VM's: one running web and the other app
(webappB)
- serverC hosts a single VM running the db function. (dbC)
- serverD hosts a single VM running the db function. (dbD)
- The service is constructed as service=svc(WEBAPP,DB), comprises
function components
WEBAPP = function(webappA,webappB) and
DB = function(dbC,dbD).
Suppose that the physical server represented by the component
serverA has an unexpected hardware failure, and webappA function
instance becomes unavailable.
The INVEST verification tool performs the following steps:
The reverification performed in Step 2 results in the new value
v_8new=0.9949.
Comparison with the old value v_8 = 1 - 1.3571E-5 yields
compare(v_8new,v_8) = 0.9949 >= 1-1.3571E-5 = false.
Since the stopping condition is not satisfied, reverification
continues to the component service1 resulting in the new
verification value
v_9new = 0.9924. None of the other components are reverified.
To improve the robustness of the service's database function, we
suppose that the system administrator deploys (or considers
deploying)
a new instance of the db function on the physical
server represented by the component serverE. The new db function
instance is
represented by the component term dbE = deploy_db(serverE).
Once we extend the properties function G_service with the mappings
serverE -> (E_1E,E_2E) and dbE -> (E_6E), for probabilistic
safety properties E_1E,E_2E and E_6E.
The INVEST incremental verification engine carries out the
following steps:
The reverification of function_db(dbC,dbD,dbE) results in the new
verification value v_7new = 1-1.2535E-4.
Comparison with the old value v_7 = 0.9975 yields
compare(v_7new,v_7) = 1-1.2535E-4 >= 0.9975 = true,
and the incremental reverification process terminates.
Suppose the administrator upgrades a physical serverA operating
web and application functions.
The physical server is represented in service2 by the
component term serverA. The INVEST incremental verification engine
carries out the following steps:
yielding new verification values
v_1new = 2.8474E-8
v_2new = 1.4171E-5
Comparisons with the old values v_1 and v_2 yields
compare(v_1new,v_1) = 1- 2.8474E-8 >= 1- 1.2326E-6
compare(v_2new,v_2) = 1- 1.4171E-5 >= 1- 4.8332E-4
and the reverification process terminates.
Suppose the administrator applies a software update that reduces
the operating reliability of the virtual machine operating
webappA instance on serverA.
The INVEST incremental verification engine carries out the
following steps:
yielding new verification values
v_3new = 0.2000 (probability of web failure)
v_4new = 0.2000 (probability of app failure)
v_5new = 0.0400 (probability of web and app functionality failing)
Comparisons with the old values v_3, v_4, v_5 yields
compare(v_3new,v_3) = 1 - 0.2000 >= 1 - 0.0500 = false
compare(v_4new,v_4) = 1 - 0.2000 >= 1 - 0.0500 = false
compare(v_5new,v_5) = 1 - 0.0400 >= 1 - 0.0025 = false
Since the reverification stopping condition is unsatisfied,
reverification continues to the component term webappDepl,
yielding the new verification value
v_8new = 0.4401.
Comparison with the old value v_8 yields
compare(v_8new,v_8) = 1 - 0.4401 >= 1 - 0.1026 = false.
Reverification continues to the component term service4, yielding
the new verification result:
v_9new = 0.4681.
Comparison with the old value v_9 yields
compare(v_9new,v_9) = 1 - 0.4681 >= 1 - 0.1475.
Thus, the overall reliability of the service is decreased as a
result of the software update.
To evaluate the performance of the INVEST tool, we ran a range of
experiments in which we started from the initial system
configuration and then changed the system over a number of
steps.
The changes in these steps involved additions of webapp and db
function instances (to assess the effect of increases in the
system size) and modifications of existing components.
The experiments were run on a standard 2.66 GHz Intel Core 2 Duo
Macbook Pro computer with 8GB of memory, and all results
(comparing the execution times of compositional and incremental
verification)
were averaged over multiple runs of each experiment.
Starting again with the initial service, we construct dbFi =
deploy_db(ServerFi) and perform the substitution
service_i = service[DB/function(dbC,dbD,dbF1,....,dbFi)] for i =
1..10.
The list of numbers below represents the performance of
compositional
verification for services i=1..20, each result represents the
average time over four runs.