We describe a generic switching protocol for the construction of hybrid
protocols and prove it correct with the 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.
The formal proofs and definitions referenced here are taken from
Hybrid Protocols.
