=ADD=
=reftype=
14
=number=
00-06
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/2000/00-06.ps.gz
=year=
2000
=month=
01
=author=
Pau; Ioana-Cleopatra + Rents; Igor + Schreiner; Wolfgang
=title=
Verifying Mutual Exclusion and Liveness Properties with TLA
=abstract=
In this paper we prove the correctness of Peterson's mutual exclusion
algorithm using the Temporal Logic of Actions (TLA).
We present a precise analysis of the algorithm for two processes:
the formal specification of the algorithm,
of the mutual exclusion property and of the liveness property and
the proof that the algorithm satisfies these two properties.
=sponsor=
FWF
=end=