This paper describes a multi-paradigm approach to formal specification and shows how this approach can be successfully used in the specification of distributed multimedia systems. We take as our example, a published description of an algorithm to establish the initial synchronisation of distributed stored media streams that avoids the need for large buffers (e.g. if the locations of the media sources are widely distributed). We show how this algorithm can be specified using a combination of real-time temporal logic and timed automata. We then describe how the different specifications (languages) can be combined in order to analyse the overall behaviour.