Proof Score for the Mutual Exclusion Property of
QLOCK
The following sequence of files shows an example process of developing
specification and proof score for the mutual exclusion property
of Qlock protocol. It is recommended for readers to check
that proof-N.mod can be
obtained
by applying legitimate splittings and/or transformations to some of
proof passage(s) in proof-(N-1).mod
for 00 < N < 22. Notice
that proof-N.mod (N = 00
... 05) is making use of only invariants-0.mod
and proof-N.mod (N = 06
... 09) is making use of only invariants-1.mod,
and proof-N.mod (N = 10
... 21) is making use of invariants-2.mod
.
- qlock.mod The
specification of the Qlock protocol as the module QLOCK
- invariants-0.mod
0th invariant file defining INV1 making use of QLOCK
- invariants-1.mod
1st invariant file defining ISTEP1 making use of INV1
- invariants-2.mod
the final invariant file defining INV2 and ISTEP2 making use of ISTEP1
and INV2 respectively.
- proof-00.mod 00th
proof
score file making use of INV1
- proof-01.mod 01th
proof
score file making use of INV1
- proof-02.mod 02th
proof
score file making use of INV1
- proof-03.mod 03th
proof
score file making use of INV1
- proof-04.mod 04th
proof
score file making use of INV1
- proof-05.mod 05th
proof
score file making use of INV1
- proof-06.mod 06th
proof
score file making use of INV1+ISTEP1
- proof-07.mod 07th
proof
score file making use of INV1+ISTEP1
- proof-08.mod 08th
proof
score file making use of INV1+ISTEP1
- proof-09.mod 09th
proof
score file making use of INV1+ISTEP1
- proof-10.mod 10th
proof
score file making use of INV1+ISTEP1+INV2+ISTEP2
- proof-11.mod 11th
proof
score file making use of INV1+ISTEP1+INV2+ISTEP2
- proof-12.mod 12th
proof
score file making use of INV1+ISTEP1+INV2+ISTEP2
- proof-13.mod 13th
proof
score file making use of INV1+ISTEP1+INV2+ISTEP2
- proof-14.mod 14th
proof
score file making use of INV1+ISTEP1+INV2+ISTEP2
- proof-15.mod 15th
proof
score file making use of INV1+ISTEP1+INV2+ISTEP2
- proof-16.mod 16th
proof
score file making use of INV1+ISTEP1+INV2+ISTEP2
- proof-17.mod 17th
proof
score file making use of INV1+ISTEP1+INV2+ISTEP2
- proof-18.mod 18th
proof
score file making use of INV1+ISTEP1+INV2+ISTEP2
- proof-19.mod 19th
proof
score file making use of INV1+ISTEP1+INV2+ISTEP2
- proof-20.mod 20th
proof
score file making use of INV1+ISTEP1+INV2+ISTEP2
- proof-21.mod the
final
proof score file making use of INV1+ISTEP1+INV2+ISTEP2.
Notice that you do not need to prepare all of the above files.
Only the files qlock.mod,
invariants-2.mod, and proof-21.mod
consititute a complete suite of specification and effective proof scroe
for the
mutual exclusion property of the Qlock protocol.
- simultaneous induction
scheme which is used to construct assertions/proof-passages in the
file proof-10.mod from the ones in the file proof-09.mod