We present a formal approach to the top-down design of real-time components that communicate using a shared data space. The approach is compositional, that is, only the formal specifications of the components are used to reason about their combined behaviour. Formal reasoning is supported by the interactive theorem prover PVS. Our shared data space model is based on the software architecture SPLICE, that allows loosely-coupled components. Our formalism is illustrated by the top-down design of a small flight-tracking-and-display system, which contains an event-driven and a time-driven component. Formal correctness is established, given suitable assumptions about the environment of the system and relations between timing parameters.