Verification of CLOUD

CLOUD |- {inv1, inv2, inv3, inv4, inv5}

We prove the following 5 invariants by simulteneous induction.

• If the status of a pc is updated then the status of cloud cannot be idle.

  ceq [inv1]: true = false if statusp(S:Sys,I:Client)= updated /\ statusc(S:Sys)= idlec .

• If the status of a pc is gotval then the status of cloud cannot be idle.

  ceq [inv2]: true = false if statusp(S:Sys,I:Client)= gotval /\ statusc(S:Sys)= idlec .

• There cannot be two pcs with the status updated.

  ceq [inv3]: true = false if statusp(S:Sys,J:Client)= updated /\ statusp(S:Sys,I:Client)= gotval .

• There cannot be two different pcs with the status gotval.

  ceq [inv4]: true = false if (I:Client ~ J:Client) = false /\ statusp(S:Sys,J:Client)= gotval /\ statusp(S:Sys,I:Client)= gotval .

• There cannot be two different pcs with the status updated.

  ceq [inv5]: true = false if (I:Client ~ J:Client) = false /\ statusp(S:Sys,J:Client)= updated /\ statusp(S:Sys,I:Client)= updated .

CLOUD + {inv1, inv2, inv3, inv4, inv5} |- inv6

• The invariant inv6 says that if a pc has gotval status then its temporal value is equal to the cloud value.

  ceq tmp(S:Sys,I:Client) = valc(S:Sys) if statusp(S:Sys,I:Client) = gotval .

  See inv6.maude for the proof.

CLOUD + {inv1,inv2,inv3,inv4,inv5,inv6} |- goal

• If the status of a pc is updated then its value is equal to the cloud value.

  crl ceq valp(S:Sys,I:Client)= valc(S:Sys) if statusp(S:Sys,I:Client)= updated .
  

  See goal.maude for the proof.