Browse Theses

In networks of communicating processes, it is often useful to prove certain "safety" properties. That is, we would like to be able to make the statement, "If two processes communicate, the messages they send will be the right ones." There have been many ad hoc proof methods proposed--almost as many methods as networks. In this dissertation, we attempt to unify the approach to verification by demonstrating an extremely flexible and robust proof technique.

We give concise formal proofs for a wide variety of networks. In some cases, these networks exhibit properties which make the use of the technique quite stratighforward. The method is also shown to be worthwhile for specification of the network behavior, just as pre and postconditions may be useful for specifying sequential procedures. None of the proofs requires the use of temporal logic.

Finally, we demonstrate that in addition to being usable, in the sense that it is feasible in many and varied instances, the proof technique is also useful, in the sense that it is easy to use, natural for message-passing networks, and modular, i.e., the proofs of individual process functions are separated from the overall network proof.