Process algebra needs proof methodology
Wan J. Fokkink, Jan Friso Groote, Reniers · TU/e Research Portal · 2004
Abstract This note contains the contribution to the Concurrency Column of the EATCS Bulletin of February, 2004. It indicates on the one hand what the strengths of process algebras are, and on the other hand mentions a major shortcoming. Using elementary process algebra it is hard to prove correctness of complex distributed algorithms, protocols and systems. We encountered this when providing a process algebraic proof that the sliding window protocol of buffer size n is behaviourally equivalent to a bounded queue of size 2n. We used and developed notions such as invariants, cones and foci and coordinate transformations together providing the means to give a precise and insightful proof of the correctness of the sliding window protocol. These and other techniques are all shortly addressed in this note. The main message however is that in order to make process algebra the universal tool for the study of correct system behaviour (for which we believe it is one of the best candidates) much more of effective proof techniques need to be developed.