We present a new structuring and verification method for (distributed) algorithms. The basic idea is that an algorithm to b e verified is stepwise transformed into a high level specification through a numb er of steps, so called coarsements. At each step some mechanism of the algorithm is identified and removed while the basic computation of the original algorithm is preserved. Only the essential parts of the algorithm are then left for verification. The method will be formalized within the refinement calculus. We will exemplify the method by verifying a distributed algorithm for minimum-hop route maintenance due to Chu [4].
| Original language | English |
|---|
| Publisher | Åbo Akademi University |
|---|
| Publication status | Published - 1994 |
|---|
| MoE publication type | D4 Published development or research report or study |
|---|
| Name | Reports on Computer Science and Mathematics, Series A94 - 156 |
|---|