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.
Chapter PDF
Similar content being viewed by others
Keywords
References
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.
Alur R., Courcoubetis C. and Dill D. L. (1993), Model-cheking in dense real-time, Information and Computation 104, pp. 2–34.
Alur R. and Dill D. L. (1990), Automata for modelling real-time systems, in Proc. ICALP’90 LNCS 443, Springer-Verlag, pp. 323–335.
Mur R. and Dill D. L. (1994), A theory of timed automata, Theoretical Computer Science, 126, pp. 183–235.
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.
Alur R. and Henzinger T. A. (1993), Real-time logics: complexity and expressiveness, Information and Computation, 104, pp. 35–77.
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.
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.
Bergstra J. A. and Klop J. W. (1984), Process algebra for synchronous communication, Information and Control, 60.
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.
Brand D. and Zafiropulo P. (1983), On communicating finite state machines, Journal of ACM, 30, pp. 361–371.
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.
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.
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.
Henzinger T. A., Manna Z. and Pnueli A. (1991a), Timed transition systems, in Proc. REX Workshop, LNCS 600, Springer Verlag, pp. 226–251.
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.
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.
Merlin P. and Faber D. J. (1976), Recoverability of communication protocols, IEEE Trans. Comm, 24.
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.
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.
Rafiq O. and Cacciari L. (1995), Protocoles, contraintes temporelles et validation, in Proc. of CFIP’95, Hermès, Paris, France, pp. 257–292.
Ramchandani C. (1974), Analysis of asynchronous concurrent systems by timed Petri nets, Tech. Rep. 120, Project MAC, MIT.
Shaw A. C. (1992), Communicating real-time state machines, IEEE Tans. Soft. Eng., 18, pp. 805–816.
West C. H. (1978), An automated technique of communications Protocol Validation, IEEE Trans. Comm., 26, pp. 1271–1275.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Cacciari, L., Rafiq, O. (1996). A temporal reachability analysis. In: Dembiński, P., Średniawa, M. (eds) Protocol Specification, Testing and Verification XV. PSTV 1995. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-34892-6_3
Download citation
DOI: https://doi.org/10.1007/978-0-387-34892-6_3
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2925-1
Online ISBN: 978-0-387-34892-6
eBook Packages: Springer Book Archive