Abstract
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.
Résumé
Avec l’émergence des systèmes répartis multimédias, les contraintes temporelles sont devenues une caractéristique essentielle à prendre en compte dans la spécification et la validation des systèmes répartis. Une approche pour la spécification et la validation de protocoles de bout-en-bout soumis à des contraintes temporelles a déjà été développée. Cette méthode fondée sur l’analyse d’accessibilité, consiste à construire un graphe d’accessibilité temporelle décrivant la communication entre deux machines temporelles à travers deux canaux FIFO temporels. La structure et les états de ce graphe sont ensuite examinés à la lumière de propriétés de communication données, pour valider le protocole sous-jacent. L’article propose une généralisation pour la description et la validation de protocoles multimédias impliquant plus de deux machines temporelles communiquant soit à travers des canaux fifo temporels, soit par rendez-vous. Deux exemples de tels protocoles sont considérés comme étude de cas.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Alur (R.), Courcoubertis (C), Halbwachs (N.), Dill (D. L.) Wono-Toi (H.). Minimization of timed transition systems, in:Proceedings of concur’92, Stony Brook, NY, USA, Springer-Verlag, vol. 630 oflncs, pages 340–354, (1992).
Alur (R.),Dill (D. L.). Automata for modelling real-time systems, in: M. S. Paterson, Ed.,Proceedings of icalp’90, Springer-Verlag, vol. 443 oflncs, p. 323–335, (1990).
Alur (R.), Dill (D.L.). The theory of timed automata, in:Realtime: theory and practice, REX workshop, Mook, The Netherlands, Springer-Verlag, vol. 600 of lncs, pp. 45–73, (1991).
Alur (R.), Dill (D.L.). A theory of timed automata,Theoretical Computer Science,126, pp. 183–235, (1994).
Aspvall (B.),Shiloach (Y.), A polynomial time algorithm for solving systems of linear inequalities with two variables per inequality, in :Proceedings of the 20th Ann. Symp. on Foundation of Computer Science, IEEE, pp. 205–217, (1979).
Brand (D.), andZafiropulo (P.). On communication finite state machine.Journal of the ACM,30, pp. 361–371, (1983).
Cacciari (L.),Rafiq (O.). On improving reduced reachability analysis, in : M. Diaz and R. Groz, Eds,Proceedings of the Fifth IF1P International Conference on Formal Descriptions Techniques (FORTE’92), ifip, North-Holland, pp. 133–147, (Oct. 1992).
Cacciari (L.), Rafiq (O.). Decidability issues in reduced reachability analysis, in:Proceedings of the IEEE International Conference on Network Protocols, San Francisco, California, USA, IEEE, pp. 158–165, (Oct. 1993).
Cacciari (L.), Rafiq (O.). Modeling and analysis of temporal constraints in communication protocols, Ann. Télécommun.,50, n° 11–12 pp. 907–919, (1995).
Cacciari (L.), Rafiq (O.). Validation of protocols with temporal constraints,Computer Communications,19. pp. 1188–1199, (1996).
Dill (D.L.). Timing assumptions and verification of finite-state concurrent systems, in :Proceedings of CAV’89, Grenoble, France, June 1989, Springer-Verlag , vol. 407 of lncs, pp. 197–212, (1989).
Floyd (R.W.), Algorithm 97, shortest path,Comm. acm,5, p. 345, (1962).
Leboucher (L.),Najm (E.). A framework for real-time Qos in distributed systems, in :Proceedings of the IEEE Workshop on Middleware for Distributed Real-Time Systems and Service, December 2-7, 1997, San Francisco, California, USA, (1997).
West (C.H.). General techniques for communication protocol validation,IBM J. Res. Develop.,22 pp. 393–404, (1978).
Author information
Authors and Affiliations
Corresponding authors
Rights and permissions
About this article
Cite this article
Cacciari, L., Omar, R. Temporal validation of multimedia protocols. Ann. Télécommun. 55, 31–44 (2000). https://doi.org/10.1007/BF02997770
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF02997770
Key words
- Communication protocol
- Multimedia service
- Time analysis
- Validation
- Distributed system
- Reachability
- Formal description technique
- Graph method
- Finite automation