The development of distributed algorithms offers challenges in verifying that they meet their specifications. The correct-by-construction approach consists in developing a model of the algorithm before transforming this model into a program. This transformation can introduce errors that were not present in the model. Our objective is to develop an automatic transformation of distributed algorithm Event-B [2] models into DistAlgo [7] programs. The Event-B language combines refinement techniques and state based modelling and is adapted to the verification of distributed systems [3,12]. The DistAlgo language is a high-level programming language for distributed algorithms. Its high-levelness makes DistAlgo closer to the mathematical notations of Event-B and improves the clarity of DistAlgo programs. A verified automatic transformation ensures that the properties proved in the model still hold in the program and facilitates the developing process.
展开▼
