The grid computing environment is proposed as a way to enhance the efficiency of the underlying system by maximizing utilization of distributed resources. Dynamic resource allocation algorithms are used to dynamically allocate suitable resources to users' tasks. The efficiency of these algorithms is then vital for both the usability of the Grid system and fulfilling its objective. In this paper, we define a formal model of a Grid system suitable for a formal analysis of resource allocation algorithms in Grid computing. We also discuss the use of information which is available to resource allocation algorithms developers, such as researchers and students, who do not have access to an internal Grid to compute the efficiency of their algorithms.