Proving Hybrid Protocols Correct

unofficial copies [PDF], [PS]


by Mark Bickford, Christoph Kreitz, Robbert van Renesse, and Xiaoming Liu

Proceedings of 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'01), R. Boulton and P. Jackson (eds.), LNCS 2152, pp. 105-120, Springer-Verlag, 2001.

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 meta-properties 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.