Date: April 1996
Pages: 77
The verification of concurrent systems, consisting of many identical finite-state machines, has gained a lot of research interest recently. One reason is the growth of data communication networks, where millions of computers use the same finite-state protocol to communicate with each other. In this report we present an induction theorem for ring protocols, consisting of an arbitrary number of identical processes, described using Pr/T-nets. Applying the proposed method temporal properties of protocols, using addresses in communication, can be verified. This has not been possible with induction methods published earlier, because the behaviour of the processes, using addresses in rings of different sizes, has not been considered identical. Using symmetries of the reachability graph of the Pr/T-net of a verified system, we abstract the addresses used by the processes away from the observable behaviour of the system, before the identity of the processes is examined. As an example we show that a starvation-free solution to the dining philosophers' problem is correct with any number of philosophers. In addition, we show that the arbitration algorithm of the Frame Synchronized Ring is fair, whatever the number of nodes is in the ring, using the assumption that every node is continuously ready to send. The arbitration algorithm of the FSR cannot be successfully verified using methods that have been published earlier.
Keywords: Concurrent and distributed systems, Frame Synchronized Ring, induction theorems, protocol verification, predicate/transition nets.