Abstract
Specifications of protocols usually involve several parameters, for example the number of retransmissions or the timeout delays. The properties satisfied by the protocol depend often on the relation between these parameters. Automatic synthesis of such relations becomes a difficult problem when the constraints are too complex, e.g., non-linear expressions between integer and/or real parameters. This paper reports about modeling and constraint synthesis in the Pragmatic General Multicast (PGM) protocol. The property that we aim to satisfy is the full reliability property for data transmission. The complexity of the PGM prevents us from doing automatic synthesis of this constraint. Instead, we propose a methodology to deal with this problem using classical model-checking tools for timed and finite systems. Our methodology consists of several steps. First, we identify the sources of complexity and, for each source, we propose several abstractions preserving the full reliability property. Then, we build an abstract parameterized model on which we test, after instantiation of parameters, that the basic properties of the protocol (deadlock freedom, liveness) are preserved. By analyzing the scenario which invalidate the full reliability property, we find a non-linear constraint between the parameters of the protocol. We check the relation found by instantiating the parameters with relevant values and applying model-checking.
This work was supported in part by the European Commission (FET project ADVANCE, contract No IST-1999-29082).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Annichini, A., Asarin, E., Bouajjani, A.: Symbolic techniques for parametric reasoning about counter and clock systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 419–434. Springer, Heidelberg (2000)
Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: ACM Symposium on Theory of Computing, pp. 592–601 (1993)
Bérard, B., Bouyer, P., Petit, A.: Analysing the pgm protocol with uppaal. In: Pettersson, P., Yi, W. (eds.) Proceedings of the 2nd Workshop RT-TOOLS, Copenhagen, Denmark (August 2002)
Bouajjani, A., Collomb-Annichini, A., Lackneck, Y., Sighireanu, M.: Analysing fair parametric extended automata analysis. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, p. 335. Springer, Heidelberg (2001)
Bouajjani, A., Collomb-Annichini, A., Sighireanu, M.: Trex: A tool for reachability analysis of complex systems. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 368. Springer, Heidelberg (2001)
Bozga, M., Fernandez, J.-C., Girvu, L., Graf, S., Krimm, J.-P., Mounier, L.: If: A validation environment for times asynchronous systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 543–547. Springer, Heidelberg (2000)
Boigelot, B., Latour, L.: ADVANCE Project Deliverable Report, chapter Verifying PGM with infinitely many packets. LIAFA (2002)
Boigelot, B.: Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, University of Liège (1998)
Boyer, M.: On modeling and verifying the pgm protocol. Technical report, LIAFA (2002)
Bultan, T.: Automated symbolic analysis of reactive systems. PhD thesis, University of Maryland (1998)
Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional mu-calculus. In: Proceedings of the 1st LICS, pp. 267–278 (1986)
Esparza, J., Maidl, M.: ADVANCE Project Deliverable Report, chapter Verifying PGM with infinitely many topologies. LIAFA (2002)
Fernandez, J.-C., Garavel, H., Kerbrat, A., Mateescu, R., Mounier, L., Sighireanu, M.: Cadp (cæsar/aldebaran development package): A protocol validation and verification toolbox. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 437–440. Springer, Heidelberg (1996)
Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.: Linear parametric model checking of timed automata. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 189. Springer, Heidelberg (2001)
Kozen, D.: Results on the propositional μ-calculus. Theoretical Computer Science 27, 333–354 (1983)
Mateescu, R., Sighireanu, M.: Efficient on-the-fly model-checking for regular alternation-free mu-calculus. In: Proceedings of the 5th International Workshop on Formal Methods for Industrial Critical Systems FMICS 2000, Berlin, Germany (April 2000)
Pettersson, P., Larsen, K.G.: Uppaal2k. Bulletin of the European Association for Theoretical Computer Science 70, 40–44 (2000)
Speakman, T., Farinacci, D., Crowcroft, J., Gemmell, J., Lin, S., Leshchiner, D., Luby, M., Tweedly, A., Bhaskar, N., Edmonstone, R., Montgomery, T., Rizzo, L., Sumanasekera, R., Vicisano, L.: PGM reliable transport protocol specification. RFC 3208, IETF, 111 pages (December 2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boyer, M., Sighireanu, M. (2003). Synthesis and Verification of Constraints in the PGM Protocol. In: Araki, K., Gnesi, S., Mandrioli, D. (eds) FME 2003: Formal Methods. FME 2003. Lecture Notes in Computer Science, vol 2805. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45236-2_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-45236-2_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40828-4
Online ISBN: 978-3-540-45236-2
eBook Packages: Springer Book Archive