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.
|Title of host publication||Algebraic Methodology and Software Technology (Proceedings 6th International Conference, AMAST'97, Sydney, Australia, December 13-17, 1997)|
|Publication status||Published - 1997|
|Name||Lecture Notes in Computer Science|