Abstract
State space explosion is a key problem in the analysis of finite state systems. The sweep-line method is a state exploration method which uses a notion of progress to allow states to be deleted from memory when they are no longer required. This reduces the peak number of states that need to be stored, while still exploring the full state space. The technique shows promise but has never achieved reductions greater than about a factor of 10 in the number of states stored in memory for industrially relevant examples. This paper discusses sweep-line analysis of the connection management procedures of a new Internet standard, the Datagram Congestion Control Protocol (DCCP). As the intuitive approaches to sweep-line analysis are not effective, we introduce new variables to track progress. This creates further state explosion. However, when used with the sweep-line, the peak number of states is reduced by over two orders of magnitude compared with the original. Importantly, this allows DCCP to be analysed for larger parameter values.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Billington J., Gallasch G.E., Kristensen L.M., Mailund T. (2004). Exploiting equivalence reduction and the sweep-line method for detecting terminal states. IEEE Trans. Systems, Man Cybernetics, Part A: Systems Humans 34(1): 23–37
Christensen, S., Kristensen, L.M., Mailund, T.: A sweep-line method for state space exploration. In Proceedings of TACAS 2001. Lecture Notes in Computer Science, vol. 2031, pp. 450–464. Springer, Heidelberg (2001)
CPN ML: An extension of standard ML. http://www.daimi.au.dk/designCPN/sml/cpnml.html
Emerson E.A., Sistla A.P. (1996). Symmetry and model checking. Formal Methods System Design 9(1/2): 105–131
Gallasch, G.E., Billington, J.: Using parametric automata for the verification of the stop-and-wait class of protocols. Proceedings of ATVA’05. Lecture Notes in Computer Science, vol. 3707, pp. 457–473. Springer, Heidelberg (2005)
Gallasch, G.E., Han, B., Billington, J.: Sweep-line analysis of TCP connection management. In Proceedings of ICFEM’05. Lecture Notes Computer Science, vol. 3785 pp. 156–172. Springer, Heidelberg (2005)
Gallasch, G.E., Billington, J., Vanit-Anunchai, S., Kristensen, L.M.: Checking safety properties on-the-fly with the sweep-line method. Int. J. Software Tools Technol. Transfer 9(3–4), 371–391 (2007) (special section on material from CPN’04 and CPN’05)
Gallasch, G.E., Ouyang, C., Billington, J., Kristensen, L.M.: Experimenting with progress mappings for the sweep-line analysis of the Internet Open Trading Protocol. In: Fifth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, DAIMI PB 570, pp. 19–38. Department of Computer Science, University of Aarhus, Aarhus October 8–11, (2004). Available via http://www.daimi.au.dk/CPnets/workshop04/cpn/papers/
Gallasch, G.E., Vanit-Anunchai, S., Billington, J., Kristensen, L.M.: Checking language inclusion on-the-fly with the sweep-line method. In: Sixth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, DAIMI PB 576, pp. 1–20. Department of Computer Science, University of Aarhus, Aarhus October 24–26, (2005). Available via http://www.daimi.au.dk/CPnets/workshop05/cpn/papers/
Godefroid P., Holzmann G.J., Pirottin D. (1995). State-space caching revisited. Formal Methods System Design 7(3): 227–241
Gordon, S., Kristensen, L.M., Billington, J.: Verification of a revised WAP wireless transaction protocol. In: Proceedings of 23rd International Conference on Application and Theory of Petri Nets, Lecture Notes Computer Science, vol. 2360, pp. 182–202. Springer, Heidelberg (2002)
Holzmann G.J. (1990). Design and Validation of Computer Protocols. Prentice Hall, New York
Holzmann G.J. (1998). An analysis of bitstate hashing. Formal Methods System Design 13(3): 287–305
Jensen K. (1996). Condensed state spaces for symmetrical coloured Petri Nets. Formal Methods System Design 9(1/2): 7–40
Jensen, K.: Coloured Petri Nets: basic concepts, analysis methods and practical use. Vol. 1, basic concepts. Monographs in Theoretical Computer Science. Springer, Heidelberg, 2nd edn. (1997)
Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri Nets and CPN tools for modelling and validation of concurrent systems. Int. J. Software Tools Technol. Transfer 9(3–4), 213–254 (2007) (special section on material from CPN04/05)
Kohler, E., Handley, M., Floyd, S.: Datagram Congestion Control Protocol, draft-ietf-dccp-spec-6. Available via http://www.read.cs.ucla.edu/dccp/draft-ietf-dccp-spec-06.txt, February (2004)
Kohler, E., Handley, M., Floyd, S.: Substantive differences between draft-ietf-dccp-spec-11 and draft-ietf-dccp-spec-12. Available via http://www.read.cs.ucla.edu/dccp/diff-spec-11-12-explain.txt, December (2005)
Kohler, E., Handley, M., Floyd, S.: Datagram Congestion Control Protocol, RFC 4340. Available via http://www.rfc-editor.org/rfc/rfc4340.txt, March (2006)
Kohler, E., Handley, M., Floyd, S.: Substantive differences between draft-ietf-dccp-spec-13 and RFC 4340. Available via http://www.read.cs.ucla.edu/dccp/diff-spec-13-rfc-explain.txt, March 2006
Kohler, E., Handley, M., Floyd, S., Padhye, J.: Datagram Congestion Control Protocol, draft-ietf-dccp-spec-5. Available via http://www.read.cs.ucla.edu/dccp/draft-ietf-dccp-spec-05.txt, October 2003
Kongprakaiwoot, T.: Verification of the Datagram Congestion Control Protocol using coloured petri nets. Master’s thesis, Computer Systems Engineering Centre, School of Electrical and Information Engineering, University of South Australia, South Australia (2004)
Kristensen, L.M., Mailund, T.: A generalised sweep-line method for safety properties. In: Proceedings of FME’02. Lecture Notes in Computer Science, vol. 2391, pp. 549–567. Springer, Heidelberg (2002)
Kristensen, L.M., Mailund, T.: Efficient path finding with the sweep-line method using external storage. In: Proceedings of ICFEM’03. Lecture Notes in Computer Science, vol. 2885, pp. 319–337. Springer, Heidelberg (2003)
Kristensen L.M., Christensen S., Jensen K. (1998). The practitioner’s guide to Coloured Petri Nets. Int. J. Software Tools Technol. Transfer 2(2): 98–132
Milner R., Harper R., Tofte M. (1990). The definition of standard ML. MIT Press, New York
Design/CPN Online. http://www.daimi.au.dk/designCPN/
Parashkevov, A.N., Yantchev, J.: Space efficient reachability analysis through use of pseudo-root states. In: Proceedings of TACAS’97, Lecture Notes in Computer Science, vol. 1217, pp. 50–64. Springer, Heidelberg (1997)
Peled, D.: All from one, one for all: on Model checking using representatives. In: Proceedings of CAV’93, Lecture Notes in Computer Science, vol. 697, pp. 409–423. Springer, Heidelberg (1993)
Valmari, A.: A stubborn attack on state explosion. In: Proceedings of CAV’90, Lecture Notes in Computer Science, vol. 531, pp. 156–165. Springer, Heidelberg (1990)
Valmari, A.: The state explosion problem. In: Lectures on Petri Nets I: Basic Models, Lecture Notes in Computer Science, vol. 1491, pp. 429–528. Springer, Heidelberg (1998)
Vanit-Anunchai, S., Billington, J.: Initial result of a formal analysis of DCCP connection management. In: Proceedings of Fourth International Network Conference (INC 2004), pp. 63–70, University of Plymouth, Plymouth, 6–9 July 2004
Vanit-Anunchai, S., Billington, J.: Effect of sequence number wrap on DCCP connection establishment. In: Proceedings of the 14th IEEE International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS), pp. 345–354 IEEE Computer Society Press, Monterey, 11–13 September 2006
Vanit-Anunchai S., Billington J. (2005). Chattering behaviour in the Datagram Congestion Control Protocol. IEE Electron. Lett. 41(21): 1198–1199
Vanit-Anunchai, S., Billington, J.: Modelling the Datagram Congestion Control Protocol’s connection management and synchronization procedures. In: Proceedings of 28th International Conference on Application and Theory of Petri Nets and other models of concurrency (ICATPN’07), Lecture Notes in Computer Science, vol. 4546, pp. 423–444. Springer, Heidelberg (2007)
Vanit-Anunchai, S., Billington, J., Gallasch, G.E.: Sweep-line analysis of DCCP connection management. In: Seventh workshop and tutorial on practical use of coloured petri nets and the CPN tools, DAIMI PB-579, pp. 157–175. Department of Computer Science, University of Aarhus, Aarhus 24–26 October (2006). Available via http://www.daimi.au.dk/CPnets/workshop06/cpn/pap-ers/
Vanit-Anunchai, S., Billington, J., Kongprakaiwoot, T.: Discovering chatter and incompleteness in the Datagram Congestion Control Protocol. In: Proceedings of FORTE’05, Lecture Notes in Computer Science, vol. 3731, pp. 143–158. Springer, Heidelberg (2005)
Wolper, P., Godefroid, P.: Partial order methods for temporal verification. In: Proceedings of CONCUR’93, Lecture Notes in Computer Science, vol. 715, pp. 233–246. Springer, Heidelberg (1993)
Wolper, P., Leroy, D.: Reliable hashing without collision detection. In: Proceedings of CAV’93, Lecture Notes in Computer Science, vol. 697, pp. 59–70. Springer, Heidelberg (1993)
Author information
Authors and Affiliations
Corresponding author
Additional information
Somsak Vanit-Anunchai was partially supported by an Australian Research Council Discovery Grant (DP0559927) and Suranaree University of Technology.
Guy Edward Gallasch was supported by an Australian Research Council Discovery Grant (DP0559927).
Rights and permissions
About this article
Cite this article
Vanit-Anunchai, S., Billington, J. & Gallasch, G.E. Analysis of the Datagram Congestion Control Protocol’s connection management procedures using the sweep-line method. Int J Softw Tools Technol Transf 10, 29–56 (2008). https://doi.org/10.1007/s10009-007-0050-1
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-007-0050-1