Introduction

Formal methods tools have greatly influenced our ability to increase the reliability of software and hardware systems by revealing errors and clarifying critical concepts. Tools such as extended type checkers, model checkers and theorem provers have been used to detect subtle errors in prototype code and to clarify critical concepts in the design of hardware and software systems. System falsification is already an established technique for finding errors in the early stages of the development of hardware circuits and the impact of formal methods has become larger the earlier they are employed in the design process.

An engagement of formal methods at an early stage of the design depends on the ability of the formal language to naturally and compactly express the ideas underlying the system. When it is possible to precisely define the assumptions and goals that drive the system design, then a theorem prover can be used as a design assistant that helps the designers explore in detail ideas for overcoming problems or clarifying goals. This formal design process can proceed at a reasonable pace, if the theorem prover is supported by a sufficient knowledge base of basic facts about systems concepts that the design team uses in its discussions.

The Logical Programming Environment (LPE) [#!bo:Constable+86a!#,#!inp:Allen+00a!#] is a framework for the development of formalized mathematical knowledge that is well suited to support such a formal design of software systems. It provides an expressive formal language and a substantial body of formal knowledge that was accumulated in increasingly large applications, such as verifications of a logic synthesis tool [#!inp:AagaardLeeser93a!#] and of the SCI cache coherency protocol [#!inp:Howe96a!#] as well as the verification and optimization of communication protocols [#!inp:KreitzHaydenHickey98a!#,#!inp:HickeyLynchvanRenessee99a!#,#!inp:BickfordHickey99a!#,#!inp:Kreitz99a!#,#!inp:Liu+99a!#].

We have used the LPE and its database of thousands of definitions, theorems and examples for the formal design of an adaptive network protocol for the Ensemble group communication system [#!RBHVK98!#,#!phd:Hayden98a!#,#!inp:Liu+01a!#]. The protocol is realized as a hybrid protocol that switches between specialized protocols. Its design was centered around a characterization of communication properties that can be preserved by switching. This led to a study of meta-properties, i.e.properties of properties, as a means for classifying those properties. It also led to the characterization of a switch-invariant that an implementation of the switch has to satisfy to preserve those properties.

In this paper we show how to formally prove such hybrid protocols correct. In Section 2 we describe the basic architecture of hybrid protocols that are based on protocol switching. We then discuss the concept of meta-properties and use it to characterize switchable properties, i.e. properties of communication protocols that can be preserved by switching (Section 4.5). In Section 4 we will give a formal account of communication properties and meta-properties as a basis for the verification of hybrid protocols with the system. In Section 5.3 we develop the switch-invariant for switching protocols and formally prove that switchable properties are preserved by switching whenever the switching protocol satisfies this invariant.