Verification of Distributed Real-Time and Fault-Tolerant Protocols
Appeared in: Proceedings 6th International AMAST Conference,
LNCS 1349, Springer-Verlag, pages 261-275, 1997.
An assertional method to verify distributed real-time and fault-tolerant protocols is presented.
To obtain mechanical support, the verification system
General PVS theories are developed to deal with timing and failures.
As a characteristic example, we verify a processor-group
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.