Static Analysis of Distributed Systems : An Approach

The paper introduces an approach to static analysis of distributed systems. It is motivated by Dijkstra's weakest precondition calculus. Dijkstra developed it originally for reasoning about the correctness of the sequential programs. We propose to extend the proof technology into the realm of distributed systems. Another goal is to reason formally about the possible behaviors of a system consisting of distributed components. The contribution of the paper is the development of a style of modeling and reasoning about the properties that allows for a straightforward and thorough analysis of distributed systems. The well-known dining philosophers problem serves as an illustration for the notation.