This report deals with the development of a general framework for Compositional Backwards Reachability (CBR) and with the verification of reachability properties on Timed Automata Networks (TAN). The CBR method is developed on the basis of a series of finer and finer partitionings of the state-space. Two different CBR algorithms are presented and proven correct. The domain of TAN, which is a real-time model, is described. The symbolic DBM-based analysis of Timed Automata used in existing verification tools, like Uppaal is explained. The second of the CBR algorithms is applied to the domain of TAN. Several extensions to the domain are discussed, and a test implementation of the basic method is developed. This implementation is used to obtain some experimental results. Finally future work is discussed and a conclusion is drawn.