An Undergraduate Course on Protocol Engineering – How to Teach Formal Methods Without Scaring Students

  • Manuel J. Fernández-Iglesias
  • Martín Llamas-Nistal
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3294)


At a first sight, teaching formal methods to future telecom engineers seems to be a simple task. Last-year engineering undergraduates have already taken demanding courses on Mathematics, Computer Science and Computer Networking, among other engineering-related subjects. Consequently, they should be prepared both for the theoretical foundations of formal methods and to apply them to practical problems. The benefits of formal methods would be evident, and students would rush to register in this course. However, when we designed a course shaped as the rest of the courses in our engineering school, it was a complete failure. This paper discusses this experience, and how it was re-engineered into a successful one to conclude that protocol engineering serves to teach formal methods without scaring students.


Protocol engineering undergraduate courses Promela Spin case-based learning 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Burguillo-Rial, J.C., Fernández-Iglesias, M.J., González-Castaño, F.J., Llamas-Nistal, M.: Heuristic-Driven Test Case Selection from Formal Specifications. A Case Study. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 436–448. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  2. 2.
    Fernández-Iglesias, M.J., Burguillo-Rial, J.C., González-Castaño, F.J., Pousada-Carballo, J.M., Llamas-Nistal, M., Romero-Feijoo, A.: Wireless Protocol testing and validation supported by formal methods. A hands-on report. The Journal of Systems and Software (2004) (to appear)Google Scholar
  3. 3.
    González-Castaño, F.J., García-Reinoso, J.: Survibable Bluetooth Location Networks. In: Procs. of IEEE Int. Conf. on Communications (2003)Google Scholar
  4. 4.
    Holzmann, G.: Design and Validation of Computer Protocols. Prentice Hall, Englewood Cliffs (1991)Google Scholar
  5. 5.
    Holzmann, G.: The Model Checker Spin. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)CrossRefMathSciNetGoogle Scholar
  6. 6.
    Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual. Pearson Education, Englewood Cliffs, New Jersey (2003)Google Scholar
  7. 7.
    Information Processing Systems - Open Systems Interconnection. LOTOS: A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. IS 8807, ISO (1989)Google Scholar
  8. 8.
    Information Processing Systems - Open Systems Interconnection. ESTELLE: A Formal Description Technique Based on an Extended State Transition Model. IS 9074, ISO (1989)Google Scholar
  9. 9.
    ITU-T. SDL: Specification and Description Language. Z.100, CCITT (1993) Google Scholar
  10. 10.
    Narayanan, S., McIlraith, S.: Simulation, Verification and Automated Composition of Web Services. In: Proceedings of WWW 2002, pp. 77–88. ACM Press, New York (2002)CrossRefGoogle Scholar
  11. 11.
    Rodríguez-Hernández, P.S., González-Castaño, F.J., Pousada-Carballo, J.M., Fernández-Iglesias, M.J., García-Reinoso, J.: Cellular Network for Real-Time Mobile Auction. Wireless Personal Communications 22(1), 23–40 (2002)CrossRefGoogle Scholar
  12. 12.
    Scacchi, W.: Process Models in Software Engineering. In: Marciniak, J. (ed.) Encyclopedia of Software Engineering, 2nd edn., Wiley, Chichester (2001)Google Scholar
  13. 13.
    Vienneau, R.: A review of Formal Methods, Kaman Sciences Corporation (1993)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Manuel J. Fernández-Iglesias
    • 1
  • Martín Llamas-Nistal
    • 1
  1. 1.Grupo de Ingeniería de Sistemas Telemáticos, Departamento de Ingeniería TelemáticaUniversidade de VigoSpain

Personalised recommendations