This work presents an integrated approach which covers from the formal specification to the analysis and use of tools to prove properties about real-time systems. The proposed language to specify the system behaviour is Timed-CSP-Z, a combination of Timed CSP and Z. We propose a rule-based strategy for converting a Timed-CSP-Z specification to TER Nets, a high level Petri Net based formalism with time. The conversion enables us to use the CABERNET tool to analyse desired properties. As a practical case study we discuss the application of this approach to the specification and analysis of an On-board Computer of a Brazilian microsatellite.