  This paper presents a fully distributed resource discovery and reservation
system. Verification of such a system is important to ensure the execution of
distributed applications on a set of resources in appropriate conditions. A
semi-formal model for his system is presented using probabilistic timed
automata. This model is timed, parametric and probabilistic, making it a
challenge to the parameter synthesis community.
