Advertisement

Teaching protocol engineering in honours year

Session 4: Formal Methods and Engineering Instruction
Part of the Lecture Notes in Computer Science book series (LNCS, volume 640)

Abstract

Protocol engineering is a branch of software engineering involved in the rigorous design, specification, verification, implementation and testing of communication protocols using formal methods. Teaching of protocol engineering in honours year (fourth year of the undergraduate course) at La Trobe University is conducted both by formal lectures and project supervision. A course by the name of “Protocol Engineering” has been taught since 1989. Students in their honours year have to do a substantial project under the supervision of a lecturer. This paper discusses the structure of the course, the experience of supervising honours projects in protocol engineering, and the improvements to be made in the future.

Keywords

Reachability Analysis Reachability Graph Conformance Testing Open System Interconnect Transport Layer Protocol 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    Advances in Petri Nets, Lecture Notes in Computer Science, Springer Verlag, 1983–1991.Google Scholar
  2. [2]
    Ang, C.C., and County, E.J.P., “Modelling the OSI FTAM Protocol”, Proceedings of the International Conference on Modelling and Simulation, Melbourne, Australia, Oct., 1987.Google Scholar
  3. [3]
    Ang, C.C., Jordan, V., and Dillon, T.S., “Application of Petri Nets to Specify and Verify ISO CASE Protocols”, Proceedings of the second International Symposium on Interoperable Information Systems, Japan, 1988.Google Scholar
  4. [4]
    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, March 1988.Google Scholar
  5. [5]
    Chiola, G., “A Software Package for the Analysis of Generalised Stochastic Petri Net Models“, Proceedings of International Workshop on Timed Petri Nets, IEEE Computer Society Press, 1985.Google Scholar
  6. [6]
    Coes, L. “Science, Mathematics, and Student Values”, Special Issue on Engineering Education, IEEE Communication Magazine, Dec., 1990.Google Scholar
  7. [7]
    Everitt, H.J., “Temporal Logic as a Query Language for PROTEAN's Reachability Graphs”, Switched Networks Research Branch Paper 147, Telecom Research Laboratories, 1988.Google Scholar
  8. [8]
    Garavel, H., Sifakis, J.,“Compilation and Verification of LOTOS Specification”, Proceedings of tenth International Symposium on Protocol Specification, Testing and Verification, North-Holland, 1990.Google Scholar
  9. [9]
    Holzmann, G.J., Design and Validation of Computer Protocols, Prentice-Hall, 1991.Google Scholar
  10. [10]
    ISO 8073, “Information Processing Systems — Open Systems Interconnection — Transport Service Protocol”.Google Scholar
  11. [11]
    ISO 8571, “Information Processing Systems — Open Systems Interconnection — File Transfer, Access and Management”.Google Scholar
  12. [12]
    ISO 8649, “Information Processing Systems — Open Systems Interconnection — Association Control Service Element”.Google Scholar
  13. [13]
    ISO 8807, “Information Processing Systems — Open Systems Interconnection — LOTOS — A formal description Technique based on Temporal ordering of observational behaviour”.Google Scholar
  14. [14]
    ISO 8824, “Information Processing Systems — Open Systems Interconnection — Specification for Abstract Syntax Notation 1”Google Scholar
  15. [15]
    ISO 8832, “Information Processing Systems — Open Systems Interconnection — Specification of the Basic Class Protocol for Job Transfer and Manipulation”Google Scholar
  16. [16]
    ISO 9041, “Information Processing Systems — Open Systems Interconnection — Virtual Terminal Protocol”Google Scholar
  17. [17]
    ISO 9066, “Information Processing Systems — Open Systems Interconnection — Reliable Transfer Service Element”Google Scholar
  18. [18]
    ISO 9074, “Information Processing Systems — Open Systems Interconnection — Estelle — A formal description Technique based on an Extended State Transition Model”.Google Scholar
  19. [19]
    ISO 9596, “Information Processing Systems — Open Systems Interconnection — Common Management Information Protocol Specification”Google Scholar
  20. [20]
    Lai, R., O'Connor, D. “Automatic Implementation of Communication Protocols Based on Petri Nets”, Proceedings of Second International Conference on Computer Network: Towards Network Globalisation, Singapore, G.S. Poo (Editor), pp103–107, World Scientific, Sept, 1991.Google Scholar
  21. [21]
    Lai, R., Kok, E. “Specification and Verification Results for ISO JTM Protocol”, Proceedings of Second International Conference on Computer Network: Towards Network Globalisation, Singapore, G.S. Poo (Editor), pp295–300, World Scientific, Sept, 1991.Google Scholar
  22. [22]
    Lai, R., Lo, A.“Specifying ISO FTAM Basic File Protocol in LOTOS”, Proceedings of Second International Conference on Computer Network: Towards Network Globalisation, Singapore, G.S. Poo (Editor), pp232–237, World Scientific, Sept, 1991.Google Scholar
  23. [23]
    Lai, R., Lo, A.,“An Analysis of ISO FTAM Basic Protocol Specified in LOTOS”, Proceedings of Fifteenth Australian Computer Science Conference, C.D. Keen (Editor), World Scientific, 1992.Google Scholar
  24. [24]
    Lai, R., Galbiati, G., “A Simulation of ISO Virtual Terminal Protocol Specified in LOTOS”, accepted for publication in the proceedings of international conference on Communication Technology to be held in Beijing, China in Sept, 1992.Google Scholar
  25. [25]
    Lai, R., Shumanov, V., “Automatic Implementation of Communication Protocol Using TOPO”, submitted to Singapore International Conference on Communication Systems to be held in September in Nov, 1992.Google Scholar
  26. [26]
    Louie, S., Lai, R., Dillon, T.S., “Test Sequence Generation for Conformance Testing of OSI Protocols”, Proceedings of Second International Conference on Communication Systems, Communication Systems: Towards Global Integration, Singapore, S.P. Yeo (Editor), pp2.3.1–2.3.5, Elsevier Science Publishers B.V., Nov., 1990.Google Scholar
  27. [27]
    Manas, J.A., de Miguel, T., “From LOTOS to C”, Proceedings of first International Conference on Formal Description Techniques, North-Holland, 1988.Google Scholar
  28. [28]
    New, D., Amer, P.D., “Protocol Visualization of Estelle Specification”, Proceedings of Third International Conference on Formal Description Techniques, North-Holland, 1990.Google Scholar
  29. [29]
    Quemada, J., Pavon, S., Fernandez, A., “Transforming LOTOS specification with LOLA: the parameterized expansion”, Proceedings of the 1st international conference on FDTs, Stirling, UK, 6–9sept. 1988, North-Holland.Google Scholar
  30. [30]
    Marsan, M.A., Balbo, G., Conte, G., “A Class of Generalised Stochastic Petri Nets for the Performance of Multiprocessor Systems,”, ACM Transactions on Computer Systems, May, 1984.Google Scholar
  31. [31]
    Petersen, J.L., Petri Nets Theory and Modelling of Systems, Prentice-Hall, Englewood Cliffs, N.J., 1981.Google Scholar
  32. [32]
    Proceedings of the Second to Eleventh International Symposium on Protocol Specification, Testing and Verification, 1982–1991, North-Holland.Google Scholar
  33. [33]
    Proceedings of the First to Fourth International Conference on Formal Description Techniques, 1988–1991, North-Holland.Google Scholar
  34. [34]
    Reisig, W., Petri Nets: An Introduction, Springer-Verlag, 1985.Google Scholar
  35. [35]
    Sifakis, J., Proceedings of First International Workshop on Automatic Verification Methods for Finite Systems”, Lecture Notes in Computer Science, Springer-Verlag, 1989.Google Scholar
  36. [36]
    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.Google Scholar
  37. [37]
    Tarnay, K., Protocol Specification and Testing, Plenum Press, 1991.Google Scholar
  38. [38]
    Tridgell, P.K., “A Study of Advanced Reachability Analysis of Numerical Petri Nets”, Switched Networks Research Branch paper 110, Telecom Research Laboratories, Australia, 1987.Google Scholar
  39. [39]
    Vuong, S.T., Cowan, D.D., “Reachability Analysis of Protocols with FIFO Channels”, SIGCOM'83 Symposium, Communication Architectures and Protocols, ACM, pp. 49–57, March, 1983.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • R. Lai
    • 1
  1. 1.Department of Computer Science and Computer EngineeringLa Trobe UniversityVictoriaAustralia

Personalised recommendations