The RT-LOTOS formal specification of the conditional delivery mechanism

摘要

The paper deals with the formal specification of a general-purpose multimedia synchronization mechanism, known as the conditional delivery mechanism capable of addressing both intraand inter-stream synchronization issues. The proposed mechanism, initially introduced in [3, 11], is based on the identification of causal relations among information units of one or several streams and has the purpose of ensuring that these causal relations, expressed at the user's level, are satisfied when delivering the streams. The formal specification of the synchronization mechanism refers to an extension of the standard formal description technique LOTOS (RT-LOTOS for Real-Time LOTOS) which adds to LOTOS the capability of expressing several time-related features.