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].
| Alkuperäiskieli | Englanti |
|---|
| Kustantaja | Åbo Akademi University |
|---|
| Tila | Julkaistu - 1994 |
|---|
| OKM-julkaisutyyppi | D4 Julkaistut kehitykset tai tutkimusraportit tai tutkimukset |
|---|
| Nimi | Reports on Computer Science and Mathematics, Series A94 - 156 |
|---|