An automatic trace analysis tool generator for Estelle specifications

ABSTRACT

This paper describes the development of Tango, an automatic generator of backtracking trace analysis tools for single-process specifications written in the formal description language, Estelle. A tool generated by Tango automatically checks the validity of any execution trace against the given specification, and supports a number of checking options. The approach taken was to modify an Estelle-to-C++ compiler. Discussion about nondeterministic specifications, multiple observation points, and on-line trace analysis follow. Trace analyzers for the protocols LAPD and TP0 have been tested and performance results are evaluated. Issues in the analysis of partial traces are also discussed.

REFERENCES

• 1: F. Belina , D. Hogrefe, The CCITT-specification and description language SDL, Computer Networks and ISDN Systems, v.16 n.4, p.311-341, March 1989 [doi>10.1016/0169-7552(89)90078-0]
• 2: O. Belial, G.v. Bochmann, M. Dubuc, and F. Saba. "Automatic test result analysis for high-level specifications". Technical Report 800, Department IRO, University of Montreal, 1991.
• 3: G.v. Bochmann, D. Ouimet, and J. Vaucher. "Performance simulation of communication protocols based on formal specifications''. Transactsons of the Society for Computer S~mulatson, 9(4):201-225, December 1992.
• 4: Tommaso Bolognesi , Ed Brinksma, Introduction to the ISO specification language LOTOS, Computer Networks and ISDN Systems, v.14 n.1, p.25-59, March, 1987 [doi>10.1016/0169-7552(87)90085-7]
• 5: R. Cork. "The testing of protocols in SNA products - an overview". In Proceedings of IFIP WG 6.1 Th2rd Annual Workshop on Protocol Specification, Testsng and Verification, 1983.
• 6: Rachida Dssouli , Reine Fournier , Gregor von Bochmann, Distributed Observation and FIFO Queues, Proceedings of the IFIP TC6/WG6.1 Third International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols: Formal Description Techniques, III, p.303-310, November 05-08, 1990
• 7: S Alan Ezust. Tango: The Trace Analys2s Generator. Master's thesis, McGill University, Montreal, Canada, 1995.
• 8: D. Hoffman , Richard Thomas Snodgrass, Trace Specifications: Methodology and Models, IEEE Transactions on Software Engineering, v.14 n.9, p.1243-1252, September 1988 [doi>10.1109/32.6168]
• 9: Gerard J. Holzmann, Design and validation of computer protocols, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 10: ISO Recommendation 90%i, The Extended State Transzt~on Language (Estelle), 1989
• 11: C. Jard and G v Bochmann. "An approach to testing specifications''. Journal of Systems and Software, 3(4), December 1983.
• 12: M.C. Kim, S. T. Chanson, and S. T Vuong. "Protocol trace analysis based on formal specifications". Technical report, University of British Columbia, Department of Computer Science, 1991.
• 13: R. Molva , Michel Diaz , Jean-Michel Ayache, Observer: a run-time checking tool for local area networks, Proceedings of the IFIP WG6.1 Fifth International Conference on Protocol Specification, Testing and Verification V, p.495-506, June 10-13, 1985
• 14: R. Probert "Towards a knowledge-based model for conformance test results analysm". In Proceedings of the IFIP WG 6. i F,fth Internat;onat Workshop on Protocol Specification, Testsng and Ver~ficatson, 1985.
• 15: P Riou. Specsficatson of the ISDN L,nk Access Protocol for D- channel (LAiOD) CCITT Recommendation Q.9~i, Centre National d'Etudes des Telecommumcations (CNET). Available by FTP on louie.udel.edu in pub/grope/estelle-specs, 1989.
• 16: B. Sarikaya , G. v. Bochmann , E. Cerny, A test design methodology for protocol testing, IEEE Transactions on Software Engineering, v.13 n.5, p.518-531, May 1987 [doi>10.1109/TSE.1987.233197]
• 17: R. Sijelmassi and B. Strausser "The distributed lmplementatlon generator, an overview and user guide". Technical report, US Department of Commerce, National Institute of Standards and Technology, N~t~on~l Computer Sy~tcm~ L~bor~tory, Sy~tcm~ and Network Architecture Division, Gaithersburg, MD 20899, 1991.
• 18: B. Strausser and J.P. Favreau. "User guide for the NBS prototype compiler for estelle" Technical Report ICST/SNA 87/3, National Institute of Standards and Technology, October 1987.
• 19: Antti Valmari, A Stubborn Attack On State Explosion, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.156-165, June 18-21, 1990
• 20: S. T. Vuong, S. Lee, and P. J Zhou. "La validation des tests de protocole: principles, outils et exemples". Acres du Colloque Francophone sur l'lngdnserse des Protocoles (CFIP), Montrdal Canada, 1993.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Tracing
  D.3 PROGRAMMING LANGUAGES

General Terms:
Design, Languages, Performance