Abstract
This paper describes the development and validation of an Estelle specification of a distributed algorithm solving the dynamic resource allocation problem. This is a modified version of the algorithm originally proposed in [Winkowski 1998]. The specification has been obtained and validated with Estelle Development Tools. The main steps in the construction of the specification are presented and the simulation techniques validating the obtained specification are sketched. The simulations show that the specification is free of dynamic errors and preserves such properties as mutual exclusion between tasks requiring the overlapping sets of resources and starvation freedom - the properties essential for any correct solution of the resource allocation problem. The full Estelle version of the algorithm is given in the Appendix.
Key words: distributed systems, multi-agent systems, distributed algorithms, resource allocation problem, Estelle specifications, validation, simulation.