Specification and Verification of Total Correctness of Distributed Programs
Michelle Nyah Joseph, Paritosh K. Pandya · Warwick Research Archive Portal (University of Warwick) · 1987
This paper describes a compositional specification and proof system for networks of distributed processes. Each process in a network is specified using first order logic in terms of a presupposition P and an affirmation A as a triple (P) S (A). For purely sequential programs, these triples reduce to the familiar Hoare triples extended for total correctness. In distributed programs, P-A triples allow the Internal behaviour of a process to be specified in the context of the communications of the other processes in the network. Communications may either by synchronous or asynchronous. Properties such as termination, the absence of deadlock and the absence of livelock can be verified. As the technique is syntax-directed and allows network abstraction, proofs follow the structure of the program and a subnetwork within a network can be replaced by a single process. It also allows proof of the properties of non-terminating processes, such as servers.