Large networks of computers supporting both local and distributed processing are emerging as the computing environments of choice. Application programs, which concurrently access shared, distributed, and possibly replicated data in these environments, need to run without interruption despite failures occurring in the system. Although distributed systems are becoming more popular, demonstrating their reliability is left up to observing their operational behavior in the field. It would be more convincing, and in the long run more cost- effective, to use a more formal means of demonstrating a system's properties than by simply observing it in use. The objectives of this project are: (1) to design specification languages suitable for describing properties of reliable distributed systems; and (2) to develop proof techniques suitable for reasoning about and guiding the development of such systems. Formal mathematics, in particular axiomatic and deductive methods of logic, will be employed to define the syntax and semantics of the languages and proof techniques. Formality will be balanced by the more pragmatic concerns of making the language expressively rich and proof techniques tractable by system developers and implementors. The results of this work will directly benefit the following communities: distributed systems, by helping people design, understand, and reason about reliable systems; programming languages, by influencing the design and semantics of future distributed languages; and formal methods, by extending axiomatic techniques to as yet unexplored grounds.
