Temporal validation of multimedia protocols

With the emergence of distributed multimedia systems, temporal constraints are becoming a fundamental feature in specifying and validating distributed systems. We have already developed an approach for specifying and validating end-to-end protocols with temporal constraints. The method based on reachability analysis, consists in constructing a temporal reachability graph describing the communication between two temporal machines through two temporal FIFO channels. The structure and states of this graph are then studied according to given communication properties to validate the related protocol. In this paper, we show how to genera lize this model for describing and validating multimedia protocols that are generally made up of more than two temporal machines communicating either through temporal FIFO channels or by rendezvous. Two examples of such protocols are considered as case studies.