Formally Verifying Hybrid Protocols with the Nuprl Logical Programming Environment

http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR2001-1839
unofficial copies [PDF], [PS]


by Mark Bickford, Christoph Kreitz, and Robbert van Renesse

Cornell University Technical Report 2001-1839, 2001.

Abstract

We describe a generic switching protocol for the construction of hybrid protocols and prove it correct with the Nuprl proof development system. We introduce the concept of meta-properties to characterize communication properties that can be preserved by switching and identify switching invariants that an implementation of the switching protocol must satisfy in order to work correctly. Our work shows how a theorem prover with a rich specification language can contribute to the design and implementation of verifiably correct adaptive protocols and that it can have a large impact when being engaged at the earliest stages of the design.