Formal methods have successfully been deployed in the field of telecommunications. A range of languages have emerged for this purpose including the standardized formal description techniques (FDTs) of LOTOS (see also chapter 5), Estelle and SDL (see also chapter 4). Furthermore, there has been significant interest in applying such techniques in the more general area of distributed systems, as reported in the first three chapters of this book. Whilst considerable progress has been made towards this goal, it is crucial that such techniques evolve to meet the new challenges of distributed systems such as multimedia, mobile computing, and the emergence of object-oriented or component-based approaches. This chapter focuses exclusively on the impact of multimedia on the formal specification of distributed systems. More specifically, the aims of this chapter are:

• to consider the implications of (distributed) multimedia for the field of formal specification and verification,
• to survey the existing body of work in this area (including single language, dual language and multi-paradigm approaches),
• to discuss the potential advantages of the multi-paradigm approach over the alternatives.

The chapter is structured as follows. Section 2 presents some background information on multimedia computing, with particular emphasis on quality of service management. This section also considers the resulting challenges for formal specification, including the need to specify and verify quality of service properties and, crucially, the requirement to represent and reason about key quality of service management functions. Section 3 then surveys the existing literature in this field, considering in turn single language approaches, dual language approaches and multi-paradigm approaches. Emphasis is also given to the key issue of separation of concerns in the different approaches. Following this, section 4 focuses on a multi-paradigm approach developed by the authors. In particular, a specification is presented of a QoS-managed audio stream featuring functional, non-functional and management aspects of the system. Note that this is an extension of part of the multimedia binding object example from the previous chapter. The topic of verification is considered in section 5, including consideration of model checking, reachability analysis and testing techniques. This section also considers the availability of tool support in this area. Finally, section 6 presents some concluding remarks.