On the Modeling of Distributed Systems with Weakest Precondition

This paper describes an approach to the modeling of distributed systems using Dijkstra's Weakest Precondition (WP) method. WP is a general purpose formal method based on standard predicate logic. The distributed algorithm for mutual exclusion in computer networks proposed by Ricart and Agrawala, has been considered. Comprehensive proof of properties like mutual exclusion, deadlock freedom, and starvation freedom has also been presented. The contribution of this paper is the development of a style of modeling and reasoning with WP that allows for a straightforward and thorough analysis of distributed systems. This analysis contributes to the understanding of a system and could lead to an improvement in the design of distributed systems