Synthesizing different development paradigms: Combining top-down with bottom-up reasoning about distributed systems

Abstract

Our goal is the presentation of a uniform framework for compositional reasoning about the development of distributed processes and data structures. This framework should be a synthesis because, depending on the structure of the processes involved and the verification steps required, different formalisms are most suitable for carrying out one’s reasoning. We illustrate this uniform framework by presenting a methodology for reasoning about refinement of distributed data structures, i.e., data structures implemented by means of distributed networks. Our synthesis is compositional, state-based, history-based, and contains sat style, Hoare style, trace-invariant reasoning and assumption/commitment style specifications as dialects. The resulting formalism can be unfolded as if it were a portable telescope, yielding the style required according to its degree of unfolding.