A formal system based on weakest precondition in a loop connected message passing communication protocol

摘要

The paper describes a weakest precondition based framework, establishing a formal system, in terms of the specification and verification of distributed systems. It is a general purpose formal method based on standard predicate logic. A loop-connected message passing communication protocol has been chosen, in the work, to carry out the case study. The contribution of the paper is the development of a style of modeling and reasoning that allows for a straightforward and thorough analysis of distributed systems. The analysis contributes to the understanding of a system and could lead to an improvement in the design of distributed systems.