Bisimulation analysis of SDL-expressed protocols: a case study

ABSTRACT

Faster, better networks algorithms are often being discovered, and it is desirable to be able to replace an old algorithm by a new in a manner that is completely transparent to the application using it. This paper investigates the technique for ensuring such transparency for protocols expressed in SDL, via bisimulation checking. We discuss the main issues involved in translating SDL into Concurrency Workbench, a tool for performing bisimulation checking, and illustrate the feasibility of the technique by comparing the SDL specification of the Go-Back N protocol with the family of new protocols, called Asynchronous Retransmission Go-Back- N (AR). The latter perform better in environments characterized by high error rates and/or large propagation delays.

REFERENCES

• 1: {1} B.A.N. Aulia and P.H.A. Venemans. "A Skeleton for the Specification of OSI Protocols in SDL". In Proceedings of the Fourth SDL Forum, Lisbon, Portugal, October 1989.
• 2: Ferenc Belina , Dieter Hogrefe , Amardeo Sarma, SDL with applications from protocol specification, Prentice-Hall, Inc., Upper Saddle River, NJ, 1991
• 3: {3} J. A. Bergstra and C. A. Middelburg. "Process algebra semantics of ω SDL". In Proceedings of the Second Workshop on Algebra of Communicating Processes , pages 309-346, May 1995.
• 4: Marius Bozga , Jean-Claude Fernandez , Lucian Ghirvu , Susanne Graf , Jean-Pierre Krimm , Laurent Mounier, IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems, Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems-Volume I, p.307-327, September 20-24, 1999
• 5: {5} M. Chechik. "On Interpreting Results of Model-Checking with Abstraction". (submitted for publication), May 2000.
• 6: {6} M. Chechik and W. Ding. "Lightweight Reasoning about Program Correctness". CSRG Technical Report 396, University of Toronto, March 2000.
• 7: R. Cleaveland, Tableau-based model checking in the propositional mu-calculus, Acta Informatica, v.27 n.9, p.725-747, Sep. 1990
• 8: Rance Cleaveland , Joachim Parrow , Bernhard Steffen, The concurrency workbench: a semantics-based tool for the verification of concurrent systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.36-72, Jan. 1993 [doi>10.1145/151646.151648]
• 9: {9} H. Erdogmus. "Formal Verification Based on Relation Checking in SPIN". In Workshop on Formal Methods in Software Practice, San Diego, California, January 1996.
• 10: Hakan Erdogmus, Architecture-driven verification of concurrent systems, Nordic Journal of Computing, v.4 n.4, p.380-413, Winter 1997
• 11: {11} Christian Facchi, Markus Haubner, and Ursula Hinkel. "The SDL Specification of the Sliding Window Protocol Revisited". Technical Report TUM-I9614, Technische Univerität München, 1996.
• 12: Jean-Claude Fernandez , Hubert Garavel , Alain Kerbrat , Laurent Mounier , Radu Mateescu , Mihaela Sighireanu, CADP - A Protocol Validation and Verification Toolbox, Proceedings of the 8th International Conference on Computer Aided Verification, p.437-440, August 03, 1996
• 13: Fred Halsall, Data Communications Computer Networks and Open Systems 3rd Ed., Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1992
• 14: Matthew Hennessy , Robin Milner, Algebraic laws for nondeterminism and concurrency, Journal of the ACM (JACM), v.32 n.1, p.137-161, Jan. 1985 [doi>10.1145/2455.2460]
• 15: Teruo Higashino , Kiyoshi Ninomiya , Tomohisa Kimoto , Kenichi Taniguchi , Masaaki Mori, Automated Verification of Equivalence of Protocol Machines, Proceedings of the IFIP WG6.1 Ninth International Symposium on Protocol Specification, Testing and Verification IX, p.235-246, June 06-09, 1989
• 16: Gerard J. Holzmann, Practical methods for the formal validation of SDL specifications, Computer Communications, v.15 n.2, p.129-134, March 1992 [doi>10.1016/0140-3664(92)90132-X]
• 17: {17} G. J. Holzmann. "The Theory and Practice of a Formal Method: NewCoRe".In Proc. IFIP World Computer Congress, Hamburg, Germany, August 1994. (invited paper).
• 18: Gerard J. Holzmann , Joanna Patti, Validating SDL Specifications: an Experiment, Proceedings of the IFIP WG6.1 Ninth International Symposium on Protocol Specification, Testing and Verification IX, p.317-326, June 06-09, 1989
• 19: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 20: {20} ITU-T. Specification and Description Language (SDL): ITU-T Recommendation Z.100. International Telecommunication Union, 1996.
• 21: K. G. Larsen, A context dependent equivalence between processes, Theoretical Computer Science, v.49 n.2-3, p.185-215, January 1987 [doi>10.1016/0304-3975(87)90007-7]
• 22: {22} S. Lin, Jr. D. J. Costello, and M. J. Miller. "Automatic-Repeat-Request Error-Control Schemes". IEEE Communication Magazine , 22(12):5-17, December 1984.
• 23: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 24: R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• 25: R. Milner, Communication and Concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 26: {26} Faron Moller and Perdita Stevens. "The Edinburgh Concurrency Workbench (Version 7)", September 1996.
• 27: {27} J. Parrow. "Verifying a CSMA/CD-protocol with CCS". In Proceedings of the IFIP WG6.1 Eighth International Symposium on Protocol Specification, Testing, and Verification, pages 373-384, Atlantic City, NJ, June 1988.
• 28: Hironori Saito , Toru Hasegawa , Yoshiaki Kakuda, Protocol Verification System for SDL Specifications Based on Acyclic Expansion Algorithm and Temporal Logic, Proceedings of the IFIP TC6/WG6.1 Fourth International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols: Formal Description Techniques, IV, p.511-526, November 19-22, 1991
• 29: {29} H.-A. Schneider and D. Taubner. "Process Algebra Techniques for Verification of SDL-Diagrams". In Proceedings of the Eighth International Conference on Software Engineering for Telecommunication Systems and Services, pages 107-111, Florence, Italy, March/April 1992.
• 30: {30} Telelogic. "Telelogic SDT Home Page". http: //www.telelogic.com/solution/ tools/sdt.asp, September 1998.
• 31: {31} D. Towsley. "The Stutter Go-Back-N ARQ Protocol". IEEE Transactions on Communications, COM-27(6):869-875, June 1979.
• 32: Heikki Tuominen, Embedding a Dialect of SDL in PROMELA, Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, p.245-260, September 21-24, 1999
• 33: {33} Hai Wang and Hwei Sheng Teoh. "Automatic Verification of Asynchronous Retransmission Go-Back- N ARQ Protocols Using the Concurrency Workbench". In M. Chechik, editor, Automated Verification: A Collection of Reports. University of Toronto, Technical Report CSRG-374, April 1998.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols
          Subjects: Protocol verification

Additional Classification:
  C. Computer Systems Organization
  C.4 PERFORMANCE OF SYSTEMS
      Subjects: Design studies

  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: SDL

General Terms:
Algorithms, Design, Experimentation, Languages, Measurement, Performance, Theory, Verification