Formal Specification of Distributed Multimedia Systems

The work reported in this book was carried out as part of the EPSRC/DTI sponsored Tempo Project at Lancaster University (in collaboration with BT labs). The aim of the Tempo Project was to investigate formal specification and associated verification techniques to support the development of distributed multimedia systems. The book describes the state of the art in distibuted multimedia computing, highlights requirements for the formal specification and verification of such systems, reviews the available formal specification notations and then, in the light of perceived limitations of the existing approaches, presents a new framework for formal specification of distributed multimedia systems. This framework uses LOTOS to describe the functional behaviour of systems and a real-time temporal logic, called QTL, to describe the non-functional properties.