Specification and validation of multimedia protocols using RT-LOTOS

The paper presents a new formal description technique, RT-LOTOS (real-time LOTOS) which is a temporal extension of the standard formal description technique LOTOS. After a brief and informal introduction to RT-LOTOS, the paper describes a design method of multimedia protocols based on the use of generic and reusable RT-LOTOS specification building blocks. An application in the area of multimedia synchronization is then developed as an illustration of the proposed design method. Several results, achieved by using the RT-LOTOS support tool RTL, are introduced and discussed with the purpose of formally assessing the quality of service of a lip-synchronization between audio and video streams