Verification of Distributed Real-Time and Fault-Tolerant Protocols

Appeared in: Proceedings 6th International AMAST Conference, LNCS 1349, Springer-Verlag, pages 261-275, 1997.

ABSTRACT

An assertional method to verify distributed real-time and fault-tolerant protocols is presented. To obtain mechanical support, the verification system PVS is used. General PVS theories are developed to deal with timing and failures. As a characteristic example, we verify a processor-group membership protocol, dealing with a dynamically changing network of processors and reasoning in terms of local clocks. Further we show some basic theories for the verification of the underlying synchronous atomic broadcast service.

Postscript