Abstract
We describe a generic switching protocol for the construction of hybrid protocols and prove it correct with the Nuprl proof development system. For this purpose we introduce the concept of metaproperties and use them to formally characterize communication properties that can be preserved by switching. We also identify switching invariants that an implementation of the switching protocol must satisfy in order to work correctly.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Aagaard and M. Leeser. Verifying a logic synthesis tool in Nuprl. In G. Bochmann and D. Probst, eds., Workshop on Computer-Aided Verification, LNCS 663, pages 72–83. Springer, 1993.
ACL2 home page. http://www.cs.utexas.edu/users/moore/acl2.
S. Allen, R. Constable, R. Eaton, C. Kreitz, L. Lorigo. The Nuprl open logical environment. In D. McAllester, ed., 17 th Conference on Automated Deduction, LNAI 1831, pages 170–176. Springer, 2000.
B. Alpern and F. Schneider. Recognizing safety and liveness. Distributed Computing, 2(3):117–126, 1987.
M. Bickford, C. Kreitz, R. van Renesse. Formally verifying hybrid protocols with the NUPRL logical programming environment. Technical report Cornell CS:2001-1839, Cornell University. Department of Computer Science, 2001.
K. Birman. Building Secure and Reliable Network Applications. Manning Publishing Co. and Prentice Hall, 1997.
K. Birman and R. van Renesse. Reliable Distributed Computing with the Isis Toolkit. IEEE Computer Society Press, 1994.
J. Chang and N. Maxemchuk. Reliable broadcast protocols. ACM Transactions on Computer Systems, 2(3):251–273, 1984.
E. M. Clarke, O. Grumberg, D. Peled. Model Checking. MIT Press, 1999.
R. Constable, S. Allen, M. Bromley, R. Cleaveland, J. Cremer, R. Harper, D. Howe, T. Knoblock, P. Mendler, P. Panangaden, J. Sasaki, S. Smith. Implementing Mathematics with the NUPRL proof development system. Prentice Hall, 1986.
M. Hayden. The Ensemble System. PhD thesis, Cornell University. Department of Computer Science, 1998.
J. Hickey, N. Lynch, R. van Renesse. Specifications and proofs for Ensemble layers. In R. Cleaveland, ed., 5 th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1579, pages 119–133. Springer, 1999.
D. Howe. Importing mathematics from HOL into NuPRL. In J. von Wright, J. Grundy, J. Harrison, eds., Theorem Proving in Higher Order Logics, LNCS 1125, pages 267–282. Springer, 1996.
D. Hutter, B. Langenstein, C. Sengler, J. H. Siekmann, W. Stephan, and A. Wolpers. Verification support environment (VSE). Journal of High Integrity, 1997.
Isabelle home page. http://www.cl.cam.ac.uk/Research/HVG/Isabelle.
M. Kaashoek, A. Tanenbaum, S. Flynn-Hummel, H. E. Bal. An efficient reliable broadcast protocol. Operating Systems Review, 23(4):5–19, 1989.
C. Kreitz, M. Hayden, J. Hickey. A proof environment for the development of group communication systems. In C. and H. Kirchner, eds., 15 th Conference on Automated Deduction, LNAI 1421, pages 317–332. Springer, 1998.
X. Liu, C. Kreitz, R. vanRenesse, J. Hickey, M. Hayden, K. Birman, R. Constable. Building reliable, high-performance communication systems from components. Operating Systems Review 34(5):80–92, 1999.
X. Liu, R. van Renesse, M. Bickford, C. Kreitz, R. Constable. Protocol switching: Exploiting meta-properties. In Luis Rodrigues and Michel Raynal, eds., International Workshop on Applied Reliable Group Communication. IEEE CS Press, 2001.
N. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996.
Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems. Springer, 1995.
P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984.
Nuprl home page. http://www.cs.cornell.edu/Info/Projects/NuPrl.
L. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6:85–128, 1998.
PVS home page. http://pvs.csl.sri.com.
John Rushby. Systematic formal verification for fault-tolerant time-triggered algorithms. IEEE Transactions on Software Engineering, 25(5):651–660, 1999.
R. van Renesse, K. Birman, S. Maffeis. Horus: A flexible group communication system. Communications of the ACM, 39(4):76–83, 1996.
R. van Renesse, K. Birman, M. Hayden, A. Vaysburd, D. Karr. Building adaptive systems using Ensemble. Software—Practice and Experience, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bickford, M., Kreitz, C., van Renesse, R., Liu, X. (2001). Proving Hybrid Protocols Correct. In: Boulton, R.J., Jackson, P.B. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2001. Lecture Notes in Computer Science, vol 2152. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44755-5_9
Download citation
DOI: https://doi.org/10.1007/3-540-44755-5_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42525-0
Online ISBN: 978-3-540-44755-9
eBook Packages: Springer Book Archive