Component-wise formal approach to design distributed systems

Abstract

Giving a compositional proof for progress properties of distributed systems has always been problematic. Without compositionality, the correctness of a component cannot be verified in isolation (without full knowledge of its would-be partners), which in many contexts is a severe restriction. This paper presents an approach in which properties, and in particular progress properties, can be proven compositionally.