RT-LOTOS and Its Application to Multimedia Protocol Specification and Validation.

Jean-Pierre Courtiat, Roberto C. de Oliveira

1995 · 12 citations · 0 references

Concepts

Abstract

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 introduction to Basic LOTOS, the main time-related operators of RTLOTOS are detailed step by step on small examples, and then formalized (RT-LOTOS operational semantics) . The second part of the paper shows the applicability of RT-LOTOS for the formal design of multimedia protocols. A design method based on generic and reusable specification building blocks is presented for formalizing a simple intra-stream symchronization mechanism. Various simulation results obtained with RTL (RT-LOTOS Laboratory), the tool environment supporting RT-LOTOS, are presented for assessing the quality of service of the proposed mechanism. Keywords : Formal methods, Process algebras, RT-LOTOS, Multimedia synchronization, Quality of Service 1 Introduction Formal description techniques are increasingly being recognized more and mo...