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 exlusion 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.
W pracy opisano przebieg specyfikowania w języku Estelle, a następnie symulacyjnej weryfikacji zmodyfikowanej wersji rozproszonego algorytmu (zaproponowanego w pracy (Winkowski 1998)) rozwiązującego problem dynamicznej alokacji zasobów. Zarówno konstrukcję specyfikacji, jak i jej weryfikację przeprowadzono z pomocą narzędzi Estelle Development Toolset. Pokazano główne kroki w tworzeniu specyfikacji oraz naszkicowano techniki symulacyjne użyte do jej weryfikacji. Symulacja pozwoliła na stwierdzenie braku dynamicznych błędów specyfikacji, ale przede wszystkim pokazała takie podstawowe własności dla zapewnienia poprawności każdego rozwiązania problemu dynamicznej alokacji, jak wykluczanie się zadań ubiegających się o te same zasoby i brak tzw. "zagładzania" zadań. Pełny tekst specyfikacji algorytmu w języku Estelle został zamieszczony w Dodatku.