Abstract
This paper describes the use of PROTEAN and associated methodology to verify the ISO FTAM (File Transfer, Access and Management) DIS (Draft international standard) protocol and discusses the analysis of its behaviour using PROTEAN facilities. PROTEAN is an automated validation tool developed by Telecom Australia. The formal description technique used is Numerical Petri Nets (NPNs), an extension of Petri Nets. The procedures carried out were based primarily on reachability analysis. The behaviour of the protocol as specified was compared to its service specification. There are two protocol machines specified for FTAM: the basic protocol and the error recovery protocol machines.
Chapter PDF
References
Bartoli, P.D., “The Application Layer of the Reference Model of Open Systems Interconnection”, Proceedings of the IEEE, vol. 71, no. 12, pp. 1404–1407, December, 1983.
Billington, J., Wilbur-Ham, M.C., and Bearman, M.Y., “Automated Protocol Verification”, Proceedings of the Fifth International Workshop on Protocol Specification, Testing and Verification, June, 1985.
Billington, J., Wheeler, G.R., and Wilbur-Ham, M.C., “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.
ISO DIS 8571, “Information Processing Systems — Open Systems Interconnection — File Transfer Access and Management — Parts 1,2,3 and 4”, Draft International Standard, ANSI, New York, 1986.
Lai, R., “Formal Specification and Verification of ISO FTAM Protocol”, PhD Thesis, La Trobe University, Australia, August, 1989.
Lai, R., Dillon, T.S., Parker, K.R., “Verification Results for ISO FTAM Basic Protocol”, Proceedings of Ninth Symposium on Protocol Specification, Testing and Verification, North-Holland, June, 1989.
Lewan, D., and Long, H.G., “The OSI File Service”, Proceedings of IEEE, Vol. 71, no. 12, pp. 1414–1419, December, 1983.
Peterson, J.L., “Petri Nets Theory and the Modelling of Systems”, Prentice-Hall, Englewood Cliffs, N.J., 1981.
Symons, F.J.W., “Modelling and Analysis of Communication Protocols using Numerical Petri Nets” PhD Thesis, Department of Electrical Engineering Science and Telecommunications, University of Essex, May, 1978.
West, C.H., “An Automated Tecnique of Communication Protocol Validation”, IEEE Transaction on Communications, vol. COM-26, pp.1271–1275, Aug, 1978.
Wheeler, G.R., “Numerical Petri Nets — A Definition”, Telecom Australia Research Laboratories Report 7780, Telecom Australia Research Laboratories, May, 1985.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lai, R., Parker, K.R., Dillon, T.S. (1991). On using protean to verify ISO FTAM protocol. In: Clarke, E.M., Kurshan, R.P. (eds) Computer-Aided Verification. CAV 1990. Lecture Notes in Computer Science, vol 531. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0023726
Download citation
DOI: https://doi.org/10.1007/BFb0023726
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54477-7
Online ISBN: 978-3-540-38394-9
eBook Packages: Springer Book Archive