Model Checking Optimisation Based Congestion Control Algorithms

• Autorzy: Lomuscio, A. , Strulo, B. , Walker, N.G. , Wu, P.
• Języki publikacji: EN

Abstrakty

EN

Model checking has been widely applied to the verification of network protocols. Alternatively, optimisation based approaches have been proposed to reason about the large scale dynamics of networks, particularly with regard to congestion and rate control protocols such as TCP. This paper intends to provide a first bridge and explore synergies between these two approaches. We consider a series of discrete approximations to the optimisation based congestion control algorithms. Then we use branching time temporal logic to specify formally the convergence criteria for the system dynamics and present results from implementing these algorithms on a state-of-the-art model checker. We report on our experiences in using the abstraction of model checking to capture features of the continuous dynamics typical of optimisation based approaches.

Słowa kluczowe

EN

model checking; distributed optimisation; congestion control; convergence

• Czasopismo: Fundamenta Informaticae
• Rocznik: 2010
• Tom: Vol. 102, nr 1
• Strony: 77-96
• Opis fizyczny: Bibliogr. 16 poz., tab., wykr.

Twórcy

autor

Lomuscio, A.

autor

Strulo, B.

autor

Walker, N.G.

autor

Wu, P.

• Lab of Computer Science, P.O.Box 8718, Beijing 100190, China,

Bibliografia

• [1] Bengtsson, J., Larsen, K. G., Larsson, F., Pettersson, P., Yi, W.: UPPAAL - a Tool Suite for Automatic Verification of Real-Time Systems, Proceedings of the DIMACS/SYCON Workshop on Verification and Control of Hybrid Systems III, number 1066 in LNCS, Springer Berlin, New Brunswick, New Jersey, United States, October 22-25 1995.
• [2] Cimatti, A., Clarke, E. M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella., A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking, Proceedings of the 14th International Conference on Computer-Aided Verification (CAV'02), number 2404 in LNCS, Springer Berlin, Copenhagen, Denmark, July 27-31 2002.
• [3] Clarke, E. M., Emerson, E. A., Sistla, A. P.: Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), 8(2), 1986, 244-263, ISSN 0164-0925.
• [4] Eardley, P.: Pre-Congestion Notification (PCN) Architecture, Internet-Draft draft-ietf-pcn-architecture-08, 2008.
• [5] Holzmann, G. J.: The Model Checker SPIN, IEEE Transactions on Software Engineering, 23(5), 1997, 279-295.
• [6] Jaggard, A. D., Ramachandran, V., Wright, R. N.: The Impact of Communication Models on Routing-Algorithm Convergence, Proceedings of the 29th International Conference on Distributed Computing Systems (ICDCS'09), IEEE Computer Society, Montreal, Quebec, Canada, June 22-26 2009.
• [7] Kelly, F., Maulloo, A., Tan, D.: Rate control for communication networks: shadow prices, proportional fairness and stability, Journal of the Operational Research Society, 49(3), 1998, 237-252.
• [8] Kelly, F., Voice, T.: Stability of end-to-end algorithms for joint routing and rate control, ACM SIGCOMM Computer Communication Review, 35(2), 2005, 5-12.
• [9] Lin, H.: Symbolic transition graph with assignment, Proceedings of the 7th International Conference on Concurrency Theory (CONCUR'96), LNCS 1119, Springer-Verlag, 1996.
• [10] Low, S. H., Lapsley, D. E.: Optimization flow control, I: basic algorithm and convergence, IEEE/ACM Transactions on Networking, 7(6), 1999, 861-874.
• [11] Sobeih, A., Viswanathan, M., Hou, J. C.: Check and simulate: a case for incorporating model checking in network simulation, Proceedings of the 2nd ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE'04), IEEE, San Diego, California, United States, June 22-25 2004.
• [12] Strulo, B., Walker, N., Wennink, M.: Lyapunov Convergence for Lagrangian Models of Network Control, Proceedings of the 1st EuroFGI International Conference on Network Control and Optimization (NETCOOP'07), number 4465 in LNCS, Springer Berlin, Avignon, France, June 5-7 2007.
• [13] Voice, T.: Stability of multi-path dual congestion control algorithms, Proceedings of the 1st International Conference on Performance Evaluation Methodologies and Tools (VALUETOOLS'06), ACM, Pisa, Italy, October 11-13 2006.
• [14] Walker, N., Wennink, M.: Interactions in Transport Networks, Electronic Notes in Theoretical Computer Science, 141(5), 2005, 97-114.
• [15] Wennink, M., Williams, P., Walker, N., Strulo, B.: Optimisation-Based Overload Control, Proceedings of the 1st EuroFGI International Conference on Network Control and Optimization (NET-COOP'07), number 4465 in LNCS, Springer Berlin, Avignon, France, June 5-7 2007.
• [16] Yuen, C., Tjioe, W.: Modeling and verifying a price model for congestion control in computer networks using promela/spin, Proceedings of the 8th International SPIN Workshop on Model Checking of Software (SPIN'01), number 2057 in LNCS, Springer Berlin, Toronto, Ontario, Canada, May 19-20 2001.