INVEST (INcremental VErification STrategy)


We present a tool-supported framework for the efficient reverification of component-based software systems after changes
such as additions, removals or modifications of components. The incremental verification engine at the core of our
INcremental VErification STrategy (INVEST) framework uses high-level algebraic representations of component-based
systems to identify and execute the minimal set of component-wise reverification steps after a system change.

The generality of the INVEST engine allows its integration with existing assume-guarantee verification paradigms.
We illustrate this integration for an existing technique for the assume-guarantee verification of probabilistic systems.
The resulting instance of the INVEST framework can reverify probabilistic safety properties of a cloud-deployed software
system in a fraction of the time required by compositional assume-guarantee verification alone.

Download the INVEST source code: invest-tool.zip. Installation instructions: readme.txt


Domain Specific Adaptor for INVEST - Cloud Deployed Systems

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).



Change Scenarios

We outline some change scenarios handled by the Incremental verification engine.

Function Instance Removal

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:

  1. The term service is updated using the substitution service1 =  service[webapp/function_webapp(webappB))].
  2. The sequence of terms s = seq(function_webapp(webappB), service1) that may require verification is constructed.
  3. Reverification is performed by calculating Anew1 = reverify(s,AcvResult, G_service), for compositional verification results AcvResult.

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.

Adding a Function Instance

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:

  1. The term service1 is updated by term substitution service2 = service1[database/function(dbC,dbD,dbE)]
  2. The reverification sequence s = seq(serverE,dbE,service2) is constructed.
  3. Reverification involves calculating $Anew2 = reverify(s,Anew1,G_service). Since the components serverE, dbE have not been previously verified, they are included in the reverification process.

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.

Physical Server Update

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:

  1. The term service2 is updated by term substitution service3 = service2[serverA/upgrade_dsk(serverA)],  replacing serverA with upgrade_dsk(serverA).
  2. The reverification sequence s = seq(service3,upgrade_dsk(serverA)) is constructed.
  3. Reverification is performed by calculating A3new = reverify(s,A2new,G_service)

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.

 

Updating the Virtual Machine Software

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:

  1. The term service4 is updated by term substitution service4 = service3[webappA/updateVMSoftware(webappA)], replacing the webappA instance in service3 with updateVMSoftware(webappA).
  2. The reverification sequence s = seq(service4,updateVMSoftware(webappA)) is constructed.
  3. Reverification is performed by calculating A4new = reverify(s,A3new,G_service)

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.


Tool Performance

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.

Experiment 1a  (Adding webapp Instances)

The first experiment compares the performance between compositional and incremental verification when a new physical server hosting two VMS running web and app function instances is added to WEBAPP.

We construct webappEi such that

- ServerEi hosts two VM's: one running web and the other app (webappEi).
webappEi = deploy_{app}deploy_{web}(serverEi)

and perform the substitution

service_i = service[WEBAPP/function(webappA,webppB,webappE1,....,webappEi)].

The figure represents the performance of compositional verification for services i=1..20, each result represents the average time over four runs.


Experiment 1b (Adding db Instances)


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.

Experiment Two


The second experiment compares the performance between compositional and incremental
verification when a model of a physical server is updated.

1) We add new i^th instance webappi and dbi, operating on servers Ai and Ci respectively.
   Incremental reverification is performed to carry these two changes.

2) We update the server model Ci of a database instance using one of the following options.
   a) adding a new disk block improving the reliability of the server.





   b) removing a disk block, causing a degradation in the reliability.


   We then reverify the system and compare compositional and incremental verification.



Kenneth Johnson