More Web Proxy on the site http://driver.im/

article

Free access

An automatic trace analysis tool generator for Estelle specifications

Authors:

Gregor v. BochmannAuthors Info & Claims

ACM SIGCOMM Computer Communication Review, Volume 25, Issue 4

Pages 175 - 184

https://doi.org/10.1145/217391.217428

Published: 01 October 1995 Publication History

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 and D Hogrefe. "The CCITT specification and description language SDL". Networks and I,.qDN Systems, 16, North- Holland, 1988/89.

Digital Library

[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]

T. Bolognesl and E. Brinksma. "Introduction to the iSO specification language, LOTOS" Computer Networks and ISDN Systems., 14, Elsevier Science Publishers B V (North-Holland), 1987.

Digital Library

[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]

R. Dssouli, R. Fournier, and G.v Bochmann. "Distributed observation and FIFO queues". In Proceedings of the 3rd Internatsonal Conference on Formal Descrsptson Techn2ques (FORTE 90). North-Holland, November 1990.

Digital Library

[7]

S Alan Ezust. Tango: The Trace Analys2s Generator. Master's thesis, McGill University, Montreal, Canada, 1995.

[8]

D. Hoffman and R. Snodgrass "Trace specifications: Methodology and models". IEEE Transactions on Software Engsneer, ng, 14(9), September 1988.

Digital Library

[9]

Gerard J. Holzmann. Design and Vahdatson of Computer Protocols Prentice Hall Software Series, 1991

Digital Library

[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.

Digital Library

[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, M. Diaz, and J. Ayache. "Observer: A run-time checkmg tool for local area networks" In Proceedings of IFIP WG 6.1 F~fth Annual Workshop on Protocol Specsficatson, Testing and Verification, 1985

Digital Library

[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, and E. Cerny "A test design methodology for protocol testing" IEEE Transactions on Software Engineering, 13, 1987.

Digital Library

[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]

A Valmarl. "A stubborn attack on state space explosion". In Workshop on Computer-Aided Versficat~on, DIMA C$ 90, 1990.

Digital Library

[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.

Cited By

Chang FRen JStirewalt KEgyed AFischer B(2007)Validating system properties exhibited in execution tracesProceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering10.1145/1321631.1321723(517-520)Online publication date: 5-Nov-2007
https://dl.acm.org/doi/10.1145/1321631.1321723
Bhargavan KGunter C(2005)Network Event RecognitionFormal Methods in System Design10.1007/s10703-005-3398-427:3(213-251)Online publication date: 1-Nov-2005
https://dl.acm.org/doi/10.1007/s10703-005-3398-4
Dingel JLiang H(2004)Automating comprehensive safety analysis of concurrent programs using verisoft and TXLACM SIGSOFT Software Engineering Notes10.1145/1041685.102990029:6(13-22)Online publication date: 31-Oct-2004
https://dl.acm.org/doi/10.1145/1041685.1029900
Show More Cited By

Index Terms

An automatic trace analysis tool generator for Estelle specifications
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Process validation
        Traceability
  2. Software notations and tools
    1. Formal language definitions
    2. System description languages
      1. Specification languages
2. Theory of computation
  1. Formal languages and automata theory

Recommendations

An automatic trace analysis tool generator for Estelle specifications
SIGCOMM '95: Proceedings of the conference on Applications, technologies, architectures, and protocols for computer communication

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 ...
Trace Specifications: Methodology and Models

The authors summarize the trace specification language and present the trace specification methodology: a set of heuristics designed to make the reading and writing of complex specifications manageable. Also described is a technique for constructing ...
Formalized structured analysis specifications

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGCOMM Computer Communication Review

ACM SIGCOMM Computer Communication Review Volume 25, Issue 4

Oct. 1995

345 pages

ISSN:0146-4833

DOI:10.1145/217391

Editor:
David Oran
Digital Equipment Corp., Littleton, MA

Issue’s Table of Contents

SIGCOMM '95: Proceedings of the conference on Applications, technologies, architectures, and protocols for computer communication
October 1995
372 pages
ISBN:0897917111
DOI:10.1145/217382
Chairman:
Stuart Wecker
Symmetrix, Inc.
,
Editor:
David Oran
Digital Equipment Corp., Littleton, MA

Copyright © 1995 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 October 1995

Published in SIGCOMM-CCR Volume 25, Issue 4

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

15
Total Citations
View Citations
429
Total Downloads

Downloads (Last 12 months)78
Downloads (Last 6 weeks)10

Reflects downloads up to 18 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Chang FRen JStirewalt KEgyed AFischer B(2007)Validating system properties exhibited in execution tracesProceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering10.1145/1321631.1321723(517-520)Online publication date: 5-Nov-2007
https://dl.acm.org/doi/10.1145/1321631.1321723
Bhargavan KGunter C(2005)Network Event RecognitionFormal Methods in System Design10.1007/s10703-005-3398-427:3(213-251)Online publication date: 1-Nov-2005
https://dl.acm.org/doi/10.1007/s10703-005-3398-4
Dingel JLiang H(2004)Automating comprehensive safety analysis of concurrent programs using verisoft and TXLACM SIGSOFT Software Engineering Notes10.1145/1041685.102990029:6(13-22)Online publication date: 31-Oct-2004
https://dl.acm.org/doi/10.1145/1041685.1029900
Dingel JLiang HTaylor RDwyer M(2004)Automating comprehensive safety analysis of concurrent programs using verisoft and TXLProceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering10.1145/1029894.1029900(13-22)Online publication date: 31-Oct-2004
https://dl.acm.org/doi/10.1145/1029894.1029900
Bhargavan KGunter CLee ISokolsky OKim MObradovic DViswanathan M(2002)VerisimIEEE Transactions on Software Engineering10.1109/32.98849528:2(129-145)Online publication date: 1-Feb-2002
https://dl.acm.org/doi/10.1109/32.988495
Bhargavan KGunter CKim MLee IObradovic DSokolsky OViswanathan M(2000)VerisimACM SIGSOFT Software Engineering Notes10.1145/347636.34783325:5(2-13)Online publication date: 1-Aug-2000
https://dl.acm.org/doi/10.1145/347636.347833
Bhargavan KGunter CKim MLee IObradovic DSokolsky OViswanathan MRichardson D(2000)VerisimProceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis10.1145/347324.347833(2-13)Online publication date: 1-Aug-2000
https://dl.acm.org/doi/10.1145/347324.347833
Musial M(1997)On-line timed protocol trace analysis based on uncertain state descriptionsFormal Description Techniques and Protocol Specification, Testing and Verification10.1007/978-0-387-35271-8_21(337-352)Online publication date: 1997
https://doi.org/10.1007/978-0-387-35271-8_21
Beamonte REzzati‐Jivan NDagenais M(2022)Execution trace‐based model verification to analyze multicore and real‐time systemsConcurrency and Computation: Practice and Experience10.1002/cpe.697434:17Online publication date: 4-May-2022
https://doi.org/10.1002/cpe.6974
Beamonte REzzati-Jivan NDagenais M(2021)Automated Generation of Model-Based Constraints for Common Multi-core and Real-Time Applications Using Execution TracingInternational Journal of Parallel Programming10.1007/s10766-020-00689-5Online publication date: 1-Jan-2021
https://doi.org/10.1007/s10766-020-00689-5
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents