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. The gear controller is a component in the 
control system operating in a modern vehicle, implementing the gear 
change algorithm. We give a detailed description of the formal model of 
the gear controller and its surrounding environment, and its correctness 
formalized in $46$ logical formulas 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 e.g. {\sl if $\FF_1$ (a request) becomes true at a certain 
time point, then $\FF_2$ (a response) must be guaranteed to hold within 
a given time bound}. We present a logic and a method to characterize 
and model--check such properties for networks of timed automata by 
syntactical transformation and reachability analysis. The advantage 
of this approach is that we need no additional implementation work to 
extend the existing model--checker, but simple manual syntactical 
manipulation on the system description. The method has been 
demonstrated in verifying the correctness of the gear controller 
design. It takes 2.99 seconds to check the 46 logical formulas
by \uppaal\ installed on a Pentium 75MHz PC equipped with 24 MB 
of primary memory.