Cloud

Consider a scenario where arbitrarily many PCs are connected to a Cloud in order to exchange messages – for simplicity, we treat these messages as natural values. Each of the PCs can fetch the latest value from the cloud, compare it with their own value, and update the Cloud or their own value depending on which is larger; see the Cloud in images.

Specification

See cloudr.maude for the full specification.

Verification

For the Cloud example we are interested in verifying the following property:

If a PC is in updated state, then the values of Cloud and PC agree.

This is achieved in three main steps.

1. CLOUD ⊢ {inv1, inv2, inv3, inv4, inv5}

We prove the following five invariants by simulteneous induction. Each of them shows that certain values of the attributes of the system are jointly inconsistent.

• If the status of a PC is updated, then the status of the Cloud cannot be idlec.

  ceq [inv1]: true = false if [< idlec,CV:Nat >,< updated,PV:Nat,TMP:Nat > A:MSet]: Reach .

• If the status of a PC is gotval then the status of Cloud cannot be idlec.

  ceq [inv2]: true = false if [< idlec,CV:Nat >,< gotvalue,PV:Nat,TMP:Nat > A:MSet]: Reach .

• There cannot be two PCs with the statuses updated and gotval.

  ceq [inv3]: true = false if [< CS:C-Status,CV:Nat >,< gotvalue,PV1:Nat,TMP1:Nat > < gotvalue,PV2:Nat,TMP2:Nat > A:MSet]: Reach .

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

  ceq [inv4]: true = false if [< CS:C-Status,CV:Nat >,< gotvalue,PV1:Nat,TMP1:Nat > < updated,PV2:Nat,TMP2:Nat > A:MSet]: Reach .

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

  ceq [inv5]: true = false if [< CS:C-Status,CV:Nat >,< updated,PV1:Nat,TMP1:Nat > < updated,PV2:Nat,TMP2:Nat > A:MSet]: Reach .

See inv.maude for the full proof.

2. CLOUD + {inv1, inv2, inv3, inv4, inv5} ⊢ inv6

We prove another invariant, inv6, using the five results above as lemmas.

• If a PC has the status gotval, then its temporal value is equal to the value of the Cloud.

  ceq [inv6]: CV:Nat = TMP:Nat if [< CS:C-Status,CV:Nat >, < gotvalue,PV:Nat,TMP:Nat > A:MSet]: Reach .

See inv6.maude for the full proof.

3. CLOUD + {inv1, inv2, inv3, inv4, inv5, inv6} ⊢ goal

The property of interest is formalized as follows:

• If the status of a PC is updated, then its value is equal to that of the Cloud.

  ceq [goal]: CV:Nat = PV:Nat if [< CS:C-Status,CV:Nat >, < updated,PV:Nat,TMP:Nat > A:MSet]: Reach .

See goal.maude for the full proof.