VERIFICATION OF COMMUNICATION IN DISTRIBUTED SOFTWARE SYSTEMS

Distributed software system can be considered as by far the most evolved form of computer systems. The complication of such system mainly comes from the process communication 1 . To verify the correctness of communication in distributes software systems, one has to have ways in reasoning the results of communication statements as well as in handling the complexity of control states caused by process communication. In this dissertation, proof rules for communication statements and techniques for handling complicated system control states are developed so that distributed software systems using various communication mechanisms may be verified. Our approach is demonstrated on programs written in the distributed programming language DPL defined in this dissertation.;Another important aspect of this research is in dealing with the complexity of control states caused by process communication. A Petri Net based control flow graph is integrated with the proof rules to provide data flow and control flow information. When send and receive are considered together, it is shown using such control flow graphs that the complexity caused by asynchronous communication can be effectively reduced. A system transition diagram is provided to ensure that the proof has covered all possible communication sequences.;In general, deadlock-free can be very hard to check. In this dissertation, we give examples to show how information obtained from partial correctness proof may be used in detecting deadlock caused by communication statements.;To provide process communication, two asynchronous communication statements, send and receive, are provided in DPL. Because they are flexible enough to implement various communication modules commonly seen in the distributed software system, proof rules for partial correctness are developed for these communication statements as well as for other sequential statements in DPL.