Abstract:

We are searching for improved ways to prove the correctness of distributed systems and protocols. Our investigation has led to a method that we baptise the Cones and Foci method. A parallel process is first transformed in a linear process by expanding the parallellism. By using convergent process operators, the description remains relatively small and the state space explosion is circumvented. Then, in order to prove a specification equal to an implementation, six sets of requirements need to be checked. Using this method we have proven a number of rather intricate distributed systems correct.