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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
M. Archer and C. Heitmeyer. Verifying hybrid systems modeled as timed automata: A case study. In Hybrid and Real-Time Systems (HART'97), pages 171–185. LNCS 1201, Springer-Verlag, 1997.
W.R. Brevier, W.A. Hunt, J.S. Moore, and W.D. Young. An approach to systems verification. Journal of Automated Reasoning, 5(4):411–428, 1989.
F. Cristian, H. Aghili, R. Strong, and D. Dolev. Atomic broadcast: From simple message diffusion to Byzantine agreement. Information and Computation, 118:158–179, 1995.
F. Cristian. Reaching agreement on processor-group membership in synchronous distributed systems. Distributed Computing, 4:175–187, 1991.
F. Cristian. On the semantics of group communication. In Formal Techniques in Real-Time and Fault-Tolerant Systems, pages 1–21. LNCS 1135, Springer-Verlag, 1996.
A. Dold. Representing, verifying and applying software development steps using the PVS system. In Algebraic Methodology and Software Technology (AMAST'95), pages 431–444. LNCS 936, Springer-Verlag, 1995.
J. Hooman. Specification and Compositional Verification of Real-Time Systems. LNCS 558, Springer-Verlag, 1991.
J. Hooman. Compositional verification of a distributed real-time arbitration protocol. Real-Time Systems, 6(2):173–205, 1994.
B. Jonsson and J. Parrow, editors. Formal Techniques in Real-Time and Fault-Tolerant Systems. LNCS 1135. Springer-Verlag, 1996.
L. Lamport and S. Merz. Specifying and verifying fault-tolerant systems. In Formal Techniques in Real-Time and Fault-Tolerant Systems, pages 41–76. LNCS 863, 1994.
S. Owre, J. Rushby, and N. Shankar. PVS: A prototype verification system. In 11th Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 748–752. Springer-Verlag, 1992.
S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, 1995.
J. Rushby. Systematic formal verification for fault-tolerant time-triggered algorithms. In C. Meadows and W. Sanders, editors, Dependable Computing for Critical Applications 6, pages 191–210, 1997.
N. Shankar. Mechanical verification of a generalized proctocol for byzantine fault tolerant clock synchronization. In Proceedings Formal Techniques in Real-Time and Fault-Tolerant Systems, pages 217–236. LNCS 571, Springer-Verlag, 1992.
P. Zhou and J. Hooman. Formal specification and compositional verification of an atomic broadcast protocol. Real-Time Systems, 9(2):119–145, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hooman, J. (1997). Verification of distributed real-time and fault-tolerant protocols. In: Johnson, M. (eds) Algebraic Methodology and Software Technology. AMAST 1997. Lecture Notes in Computer Science, vol 1349. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0000476
Download citation
DOI: https://doi.org/10.1007/BFb0000476
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63888-9
Online ISBN: 978-3-540-69661-2
eBook Packages: Springer Book Archive