In this paper, we report on an application of the validation and
verification tool kit UPPAAL in the design and analysis of a prototype
gear controller, carried out in a joint project between industry and
academia. We give a detailed description of the formal model of the
gear controller and its surrounding environment, and its correctness
formalised according to the informal requirements delivered by our
industrial partner of the project.  The second contribution of this
paper is a solution to the problem we met in this case study, namely
how to use a tool like UPPAAL, which only provides reachability
analysis to verify bounded response time properties.  The advantage of
our solution is that we need no additional implementation work to
extend the existing model-checker, but simple manual syntactical
manipulation on the system description.