VII.2 Runtime verification

Runtime Verification [Slide 310]

1.

Establish all desirable system properties (functional, timing, resource, …)

2.

Insert at suitable places in the source code of the system assertion points

3.

Use AnaTempura to check that the generated behaviour satisfies the desired properties

Assertion points → behaviour.

Example:  Computation of factorial.

main() 
{  long y, fac=1; 
   assertion("fac", fac); 
   text_out("Enter the seed:"); 
   scanf("%d",&y); 
   assertion("y", y); 
   while (y>1) { 
     fac=fac*y; 
     assertion("fac", fac); 
     y=y-1; 
     assertion("y", y); 
   } 
}

Will generate the following sequence of changes (seed is 4):

!PROG: assert fac:1:!
!PROG: assert y:4:!
!PROG: assert fac:4:!
!PROG: assert y:3:!
!PROG: assert fac:12:!
!PROG: assert y:2:!
!PROG: assert fac:24:!
!PROG: assert y:1:!

The corresponding behaviour (interval):

• Location of assertion points is determined by the variables used in our property of interest.
• Simple search through the source code will locate all places where the variables are changing.
• We will place the assertion points directly after those “places of change”.
• This will ensure that behaviour generated during the runtime of the system is indeed the “correct” behaviour.

The property we want to check: (Invariant of the while loop)

 define fac_rel(Y,seed) = { 
    if Y=seed then Y 
    else Y * fac_rel(Y+1,seed)   }.

The check:

define test() = { 
  exists Fac,Y,seed : { 
    { seed = 1+random mod 9 and prog_send(seed) }; 
    check(1,Fac,Y); 
    if seed>1 then { 
     while Y>1 do check(fac_rel(Y,seed),Fac,Y) 
    } else { empty  } 
    } 
}.

Where

define check(Z,X,Y) = { 
    { skip and get_var("fac",X) and stable(X) and 
      if X=Z then { 
          format("!:: Pass Prog %7d Prop %7d \n", X, Z) 
      } else { 
          format("!:: Fac: Prog %d Prop %d \n", X, Z) 
      } 
    }; 
    { skip and get_var("y",Y) and stable(X) and stable(Y)}; 
    { skip and stable(Y) } 
}.

Sample test run (seed is 10):

Tempura 1> run test().
!:: Pass Prog       1 Prop       1
!:: Pass Prog      10 Prop      10
!:: Pass Prog      90 Prop      90
!:: Pass Prog     720 Prop     720
!:: Pass Prog    5040 Prop    5040
!:: Pass Prog   30240 Prop   30240
!:: Pass Prog  151200 Prop  151200
!:: Pass Prog  604800 Prop  604800
!:: Pass Prog 1814400 Prop 1814400
!:: Pass Prog 3628800 Prop 3628800
Done!  Computation length:  30.
Total Passes:  31.
Total reductions: 4164(4164 successful).
Maximum reduction depth:  31.