Abstract
Communications protocols are examples of practical concurrent systems. Formal Description Techniques (FDTs) are being used for the specification of communication protocols to achieve greater accuracy and efficiency in their design and implementation [22]. These specifications can be analysed to verify accuracy and can be used as a rigorous basis for implementation.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
M. Y. Bearman, M. C. Wilbur-Ham and J. Billington, “A Formal Specification of the OSI Class 0 Transport Protocol using NPNs”, Telecom Australia Research Laboratories Report No. 7736 (October 1984)
M. Y. Bearman, M. C. Wilbur-Ham and J. Billington, “Analysis of the OSI Class 0 Transport Protocol using NPNs”, Telecom Australia Research Laboratories Report No. 7737 (November 1984)
M. Y. Bearman, “Formal Specification of the Open Systems Interconnection Transport Protocol Class 2, using NPNs”, CSIRONET Technical Report No. 25 (1986)
M. Y. Bearman, K. R. Parker and R. A. Berger, “A Formal Specification of the OSI Class 3 Transport Protocol using NPNs”, CSIRO Division of Information Technology, Technical Report TR-ED-88–02 (February 1988)
J. Billington, M. C. Wilbur-Ham and M. Y. Bearman, “Automated Protocol Verification”, in Protocol Specification, Testing, and Verification, V (ed. M. Diaz), North-Holland, pp. 59–70 (1986)
J. Billington, G. R. Wheeler and M. C. Wilbur-Ham, “PROTEAN: A High-Level Petri Net Tool for the Specification and Verification of Communication Protocols”, IEEE Transactions on Software Engineering, Vol. 14, No. 3, pp. 301–316 (March 1988)
G. J. Cain, K. E. Cheng, C. J. Fidge, L. N. Jackson and R.S.V. Pascoe, “Computer-Aided CHILL Code Generation Report No. 12”, RMIT Research and Development Memorandum No. 112034M, contract report to Telecom Australia Research Laboratories (Feb 1984)
CCITT, “Specification and Description Language (SDL) — Recommendations Z.100” (1986)
CCITT, “CHILL Language Definition Recommendation Z.200”, (May 1984)
K. E. Cheng, R.S.V. Pascoe, T. S. Choong, L. N. Jackson and G. J. Cain, “An Integrated Approach to Automated Telecommunications Software Development”, The First Pan Pacific Computer Conference, Melbourne (Sep 1985)
J. P. Courtiat, J. M. Ayache and B. Algayres, “Petri Nets Are Good For Protocols”, ACM SIGCOMM‘84, pp. 66–74 (June 1984)
E. W. Dijkstra, “A Discipline of Programming”, Prentice Hall (1976)
C. J. Fidge and R.S.V. Pascoe, “A Comparison of The Concurrency Constructs and Module Facilities of CHILL and Ada”, Australian Computer Journal, Vol. 15, No.1 (Feb 1983)
T. G. Freeman, “The Diagram Editor GENIE”, A USGRAPH 86 Fourth Australasian Conference on Computer Graphics, Sydney, Australia, pp. 15–19 (July 1986)
G. Freeman, “User Guide for the Diagram Editor GENIE”, CSIRO Division of Information Technology, Canberra (May 1986)
J. V. Guttag and J. J. Horning, “The Algebraic Specification of Abstract Data Types”, Acta Informatica, Vol. 10 (1978)
ISO 8072, “Information Processing Systems Open Systems Interconnection Transport Service Definition” (1986)
ISO 8073, “Information Processing Systems Open Systems Interconnection Connection Oriented Transport Protocol Specification” (1986)
ISO DIS 8571, “Information Processing Systems Open Systems Interconnection File Transfer, Access and Management” (1986)
L. N. Jackson, C. J. Fidge, R. S. V. P. Pascoe and P. H. Gerrand, “Computer-Aided Program Generation from System Specifications: Design Experience from the MELBA Project”, International Switching Symposium, Florence (May 1984)
B. Liskov and S. Zilles, “An Introduction to Formal Specifications of Data Abstractions”, Current Trends in Programming Methodology, edited by R. T. Yeh, Vol. 1, pp. 1–32, Prentice-Hall, New Jersey (1977)
K. R. Parker, “Formal Description Techniques in the Development of Open Systems Interconnection Standards”, Australian Software Engineering Conference, Canberra, Australia, pp. 267–280 (May 1988)
K. R. Parker and R. A. Berger, “The PROTGEN NPN Graphical Input and Conversion System”, CSIRO Division of Information Technology, Technical Report TR-ED-88–01 (February 1988)
K. R. Parker, R. A. Berger and M. Y. Bearman, “Analysis of Numerical Petri Net Specifications of OSI Protocols”, Australian Software Engineering Conference, Canberra, Australia, pp. 193–209 (May 1988)
F. J. W. Symons, “Modelling and Analysis of Communication Protocols using Numerical Petri Nets”, PhD. Thesis, University of Essex (May 1978)
F. J. W. Symons, “Representation, Analysis and Verification of Communication Protocols”, Telecom Australia Research Laboratories Report No. 7380 (1980)
G. R. Wheeler, “Numerical Petri Nets —A Definition”, Telecom Australia Research Laboratories Report No. 7780 (April 1985)
M. C. Wilbur-Ham, “Numerical Petri Nets —A Guide”, Telecom Australia Research Laboratories Report No. 7791 (May 1985)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1990 Springer-Verlag London
About this paper
Cite this paper
Parker, K.R., Berger, R.A., Cheng, K.E. (1990). Protocol Analysis and Implementation using NPNs and SDL. In: Rattray, C. (eds) Specification and Verification of Concurrent Systems. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3534-0_5
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3534-0_5
Publisher Name: Springer, London
Print ISBN: 978-3-540-19581-8
Online ISBN: 978-1-4471-3534-0
eBook Packages: Springer Book Archive