Advertisement

Abstract

Reachability analysis is the most popular and the most used method in protocol validation. It consists in constructing a graph called reachability graph, describing communication of machines exchanging messages through FIFO channels. The states and structure of this graph are then analysed according to given properties to validate the related communication protocol. In this paper, we go from communicating machines used in reachability analysis, to design temporal communicating machines allowing one to specify quantitative temporal aspects of communication protocols. A temporal reachability graph describing the global behavior of temporal communicating machines, is then defined. After that, we show how this graph can be used to analyse general properties of communication protocols submitted to temporal constraints.

Keywords

Protocols Modeling Transition models Temporal constraints Temporal communicating systems Temporal reachability analysis Communication properties Validation 

References

  1. Alur R., Courcoubetis C. and Dill D. L. (1990), Model-cheking for real-time systems, in Proc. 5th IEEE Symp. on Logic in Computer Science, pp. 414–425.Google Scholar
  2. Alur R., Courcoubetis C. and Dill D. L. (1993), Model-cheking in dense real-time, Information and Computation 104, pp. 2–34.MathSciNetCrossRefzbMATHGoogle Scholar
  3. Alur R. and Dill D. L. (1990), Automata for modelling real-time systems, in Proc. ICALP’90 LNCS 443, Springer-Verlag, pp. 323–335.Google Scholar
  4. Mur R. and Dill D. L. (1994), A theory of timed automata, Theoretical Computer Science, 126, pp. 183–235.MathSciNetCrossRefGoogle Scholar
  5. Alur R. and Henzinger T. A. (1991), Logics and models of real-time: a survey, in Proc. REX Workshop, LNCS 600, Springer-Verlag, pp. 74–106.Google Scholar
  6. Alur R. and Henzinger T. A. (1993), Real-time logics: complexity and expressiveness, Information and Computation, 104, pp. 35–77.MathSciNetCrossRefzbMATHGoogle Scholar
  7. Alur R., Dill D. L., Wong-Toi H., Courcoubetis C. and Halbwachs N. (1992), Minimizing of timed transition systems. in Proc. CONCUR’92, LNCS 630, Springer-Verlag, pp. 340–354.MathSciNetGoogle Scholar
  8. Aspavall B. and Shiloach Y. (1979), A Polynomial time algorithm for solving systems of linear inequalities with two variables per inequality, in Proc. 20th Ann. Symp. on Foundation of Computer Sciences, IEEE, pp. 205–217.Google Scholar
  9. Bergstra J. A. and Klop J. W. (1984), Process algebra for synchronous communication, Information and Control, 60.Google Scholar
  10. Berthomieu B. and Diaz M. (1991), Modeling and verification of time dependent systems using time Petri nets, IEEE Trans. Soft. Eng, 17, pp. 259–273.MathSciNetCrossRefGoogle Scholar
  11. Brand D. and Zafiropulo P. (1983), On communicating finite state machines, Journal of ACM, 30, pp. 361–371.MathSciNetCrossRefGoogle Scholar
  12. Courtiat J.-P. and Diaz M. (1991), Time in state-based formal description techniques for distributed systems, in Proc. REX Workshop, LNCS 600, Springer Verlag, pp. 149–175.Google Scholar
  13. Courtiat J.-P., De Camargo M. S. and Saidouni D. E. (1993), RT_LOTOS: LOTOS temporisé pour la spécification de systèmes temps réel, in Actes de CFIP’93, Hermès, Paris, France, pp. 427–441.Google Scholar
  14. Dill D. L. (1989), Timing assumptions and verification of finite-state concurrent systems, in Proc. Workshop on Automatic Verification Methods for Finite State Systems, LNCS 407, Springer Verlag, pp. 197–212.Google Scholar
  15. Henzinger T. A., Manna Z. and Pnueli A. (1991a), Timed transition systems, in Proc. REX Workshop, LNCS 600, Springer Verlag, pp. 226–251.Google Scholar
  16. Henzinger T. A., Manna Z. and Pnueli A. (1991b), Temporal proof methodologies for real-time systems, in Proc. 18th Annual ACM Symp. on Programming Languages, pp. 353–366.Google Scholar
  17. Leduc G. and Leonard L. (1993), Comment rendre LOTOS apte à spécifier des systèmes temps réel, in Actes de CFIP’93, Hermès, Paris, France, pp. 407–426.Google Scholar
  18. Merlin P. and Faber D. J. (1976), Recoverability of communication protocols, IEEE Trans. Comm, 24.Google Scholar
  19. Nicollin X. and Sifakis J. (1991), An overview and synthesis on timed process algebras, in Proc. CAV’91, LNCS 575, Springer Verlag, pp. 376–398.Google Scholar
  20. Ostroff J. S. (1989), Automated verification of timed transition models, in Proc. Workshop on Automatic Verification Méthods for Finite State Systems, LNCS 407, Springer Verlag, pp. 247–256.Google Scholar
  21. Rafiq O. and Cacciari L. (1995), Protocoles, contraintes temporelles et validation, in Proc. of CFIP’95, Hermès, Paris, France, pp. 257–292.Google Scholar
  22. Ramchandani C. (1974), Analysis of asynchronous concurrent systems by timed Petri nets, Tech. Rep. 120, Project MAC, MIT.Google Scholar
  23. Shaw A. C. (1992), Communicating real-time state machines, IEEE Tans. Soft. Eng., 18, pp. 805–816.CrossRefGoogle Scholar
  24. West C. H. (1978), An automated technique of communications Protocol Validation, IEEE Trans. Comm., 26, pp. 1271–1275.CrossRefGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 1996

Authors and Affiliations

  • Leo Cacciari
    • 1
  • Omar Rafiq
    • 1
  1. 1.Laboratoire TASC / InformatiqueUniversité de PauPauFrance

Personalised recommendations