AbstractWe present a structuring and verification method for distributed algorithms. The basic idea is that an algorithm to be verified is stepwise transformed into a high level specification through a number of steps, so-called coarsenings. At each step some mechanism of the algorithm is identified, verified and removed while the basic computation of the original algorithm is preserved. The method is based on a program development technique called superposition and it is formalized within the refinement calculus. We will show the usefulness of the method by verifying a complex distributed algorithm for minimum-hop route maintenance due to Chu.
Categories and Subject Descriptors: D.2.4 [Software Engineering]: Program Verification; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs
Additional Key Words and Phrases: verifying programs, understanding programs, distributed systems, superposition refinement, action systems
Selected references
- R. J. R. Back and J. von Wright. Trace refinement of action systems. In Bengt Jonsson and Joachim Parrow, editors, CONCUR '94: Concurrency Theory, 5th International Conference, volume 836 of Lecture Notes in Computer Science, pages 367-384, Uppsala, Sweden, 22-25August 1994. Springer-Verlag.
- Nissim Francez and Ira R. Forman. Superimposition for interacting processes. In J. C. M. Baeten and J. W. Klop, editors, CONCUR '90: Theories of Concurrency: Unification and Extension, volume 458 of Lecture Notes in Computer Science, pages 230-245, Amsterdam, The Netherlands, 27-30August 1990. Springer-Verlag.
- Shmuel Katz. A superimposition control construct for distributed systems. ACM Transactions on Programming Languages and Systems, 15(2):337-356, April 1993.
- Leslie Lamport. An assertional correctness proof of a distributed algorithm. Science of Computer Programming, 2(3):175-206, December 1982.
- Simon S. Lam and A. Udaya Shankar. Protocol verification via projections. IEEE Transactions on Software Engineering, 10(4):325-342, July 1984.