© 1989 by British Computer Society
Proving Correctness Properties of a Replicated Synchronous Program

1 Computing Laboratory, University of Newcastle upon Tyne, UK, 2 Dipartimento di Informatica, Universita di Pisa, Italy, 3 Universita di Reggio Calabria, Italy
Replicated synchronous programs executed by a set of possibly faulty processors find a natural application in the fault-tolerance technique known as N-Modular Redundancy (NMR). We present an axiomatic approach to correctness proofs for replicated synchronous programs and illustrate its application by studying an agreement protocol for NMR distributed computing.
Received April 1987. revised March 1988.
* Computing Laboratory, University of Newcastle upon Tyne
Dipartimento di Informatica, Università di Pisa, Italy