Skip to main content
SpringerLink
Log in
Book cover

International Symposium of Formal Methods Europe

FME 2001: FME 2001: Formal Methods for Increasing Software Productivity pp 436–448Cite as

From Complex Specifications to a Working Prototype. A Protocol Engineering Case Study

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2021))

Abstract

We describe our experience using Formal Description Techniques (FDTs) to support the design of interception systems for GSM networks. Both the GSM protocol and the interceptor have been specified using LOTOS, an FDT standardized by the International Standardization Organization (ISO) to describe communication systems and protocols. This has permitted us to asses the feasibility of the proposed system and speed up further design phases. From the LOTOS model, a simulator has been generated automatically. The TOPO tool set was used across the process. An FTP link to a package containing the specification and the simulator is provided.

Visiting the International Computer Science Institute, Berkeley, USA, supported by a Spanish CICYT grant.

Visiting Computer Science Department, University of Wisconsin-Madison, USA, supported by a NATO Scientific Committee Grant.

Manuel J. Fernández Iglesias was affiliated to the International Computer Science Institute, Berkeley, USA, and Javier González-Castaño was affiliated to the Computer Sciences Department, University of Wisconsin-Madison, USA, when this version was written.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bieber, P.: Formal Techniques for an ITSEC-E4 Secure Gateway, Procs. of the 12th, Annual Computer Security Applications Conference, IEEE Computer Society Press, 1996.

    Google Scholar 

  2. Bowen, J., Hinchey, M.: Seven more myths of formal methods, IEEE Software, 12(4) (1995) 34–41.

    Article  Google Scholar 

  3. Butler, R., Miller, S., Potts, J., Carreño, V. A.: A Formal Methods Approach to the Analysis of Mode Confusion, in: Procs. of the 17th AIAA/IEEE Digital Avionics Systems Conferenfce, 1998.

    Google Scholar 

  4. Easterbrook, S., Callahan, J.: Formal Methods for V&V of Partial Specifications: An Experience Report, in: Procs. of the 3rd IEEE International Symposium on Requirements Engineering (RE’97), IEEE Computer Society Press, 1997.

    Google Scholar 

  5. Ehrig, H., Mahr, B.: Fundamentals of algebraic specification 1, EATCS Monographs on Computer Science, Springer Verlag, 1985.

    Google Scholar 

  6. ETSI: GSM 03.22: Functions related to mobile station (MS) in idle mode and group receive mode, Digital cellular telecommunications system (Phase 2+) standards suite, ETSI Technical Report ETR 300 930, 1997.

    Google Scholar 

  7. ETSI: GSM 04.07: Mobile radio interface signalling layer 3. General aspects, Digital cellular telecommunications system (Phase 2+) standards suite, ETSI Technical Report ETR 300 939, 1997.

    Google Scholar 

  8. Fernáandez-Iglesias, M. J., Llamas-Nistal, M.: Algebraic Specification through Expression Transformation, in: Mizuno, T., Shiratori, N., Higashino, T., Togashi, A., (Eds.), Procs. of the Joint Conference FORTE/PSTV’97, Chapman & Hall, 1997,355–366.

    Google Scholar 

  9. González-Castaño, F. J., Romero-Feijoo, A. et al: Real-Time Interceptor for the GSM Protocol, Technical Report UV/DTC/GRPILF00, Departamento de Tecnologñas de las Comunicaciones. Universidad de Vigo, 2000.

    Google Scholar 

  10. Grant, H.: Managing electromagnetic compatibility between wireless and medical devices, Compliance Engineering, may-june (1999) 26–31.

    Google Scholar 

  11. Hall, J. A.: Seven myths of formal methods, IEEE Software, 7(5) (1990) 11–19.

    Article  Google Scholar 

  12. Hao, R., Lee, D., Sinha, R. K., Vlah, D.: Testing IP Routing Protocols. From Probabilistic Algorithms to a Software Tool, in: Bolognesi, T., Latella, D. Formal Methods for Distributed System Development, Kluwer Academic Publishers, 2000, 249–266.

    Google Scholar 

  13. Haxthausen, A. E., Peleska, J.: Formal Development and Verification of a Distributed Railway Control System, IEEE Transactions on Software Engineering, 26(8) (2000) 687–701.

    Article  Google Scholar 

  14. Hoare, C. A. R.: Communicating Sequential Processes, Prentice-Hall, 1985.

    Google Scholar 

  15. Holloway, C. M.: Why Engineers Should Consider Formal Methods, in: Procs. of the 16th AIAA/IEEE Digital Avionics Systems Conference, vol. 1, 3–16, 1997.

    Google Scholar 

  16. Holloway, C. M., Butler, R.: Impediments to Industrial Use of Formal Methods, IEEE Computer, 29(4), (1996) 25–26.

    Google Scholar 

  17. Holzmann, G.: Design and Validation of Computer Protocols, Prentice Hall, 1991.

    Google Scholar 

  18. Holzmann, G.: Proving the Value of Formal Methods, Procs. of the 7th. Intl.IFIP Conf. on Formal Description Techniques, FORTE’94, North Holland, 1994.

    Google Scholar 

  19. ISO: ESTELLE: A formal description technique based on the extended state transition model, International Standard 9074, International Standardization Organization, 1989.

    Google Scholar 

  20. Leduc, G., Bonaventure, O., Koerner E., Léonard, L., Pecheur, C., Zanetti, D.: Specification and Verification of a TTP Protocol for the Conditional Access to Services, in: Procs. of the 12th. J. Cartier Workshop on Formal Methods and their Applications, 1996.

    Google Scholar 

  21. ISO: LOTOS: A formal description technique based on the temporal ordering of observational behavior, International Standard 8807, International Standardization Organization, 1988.

    Google Scholar 

  22. ITU: SDL: Specification and Description Language, CCITT Recommendation Z.100, International Telecommunication Union, 1993.

    Google Scholar 

  23. Jonkers, V., Verschaeve, K., Wydaeghe, B., Coypers, L., Heirbaut, J.: OMT*, Bridging the Gap between Analysis and Design, in: Procs. of the 8th. Intl. IFIP Conf. on Formal Description Techniques, FORTE’95, North Holland, 1995.

    Google Scholar 

  24. Llamas-Nistal, M., Fernández-Iglesias, M. J., Burguillo-Rial, J. C., Pousada-Carballo, J. M., González-Castaño, F. J., Anido-Rifón, L.: LOTOOL: A Tool for Developing, Verifying and Testing Protocols using Formal Description Techniques, in: Innovations and Quality in Education for Electrical and Information Engineering, European Association for Education in Electronic and Information Engineering, 1997, pp. F1.18–F1.23.

    Google Scholar 

  25. Llamas-Nistal, M., Quemada, J., Fernáandez-Iglesias, M. J.: Direct Verification of Bisimulations, in: Procs. of the Joint Conference FORTE/PSTV’96, Chapman & Hall, 1996.

    Google Scholar 

  26. Mañas, J. A., de Miguel, T.: From LOTOS to C, in: K. J. Turner, (Ed), Procs. Of FORTE’88, North Holland, 1988, 79–84.

    Google Scholar 

  27. Mañas, J. A., de Miguel, T., Salvachúa, J., Azcorra, A.: Tool support to implement LOTOS specifications, Computer Networks and ISDN Systems, 25 (1993) 79–84.

    Article  Google Scholar 

  28. Mehrotra, A.: GSM System Engineering, Artech House, 1997.

    Google Scholar 

  29. Milne, G.: CIRCAL and the representation of communication, concurrency and time, ACM Trans. on Programming Languages and Systems, 7(2) (1985) 270–298.

    MATH  Google Scholar 

  30. Milner, R.: Calculus of communicating systems, Lecture Notes on Computer Science 92, Springer Verlag, 1980.

    Google Scholar 

  31. Milner, R.: Communication and Concurrency, Prentice Hall, 1989.

    Google Scholar 

  32. Mouly, M., Pautet, M.-B.: The GSM System for Mobile Communications, Cell & Sys, 1992.

    Google Scholar 

  33. de Nicola, R.: Extensional Equivalences for Transition System, Acta Informatica, 24 (1987) 211–237.

    Article  MATH  MathSciNet  Google Scholar 

  34. Pousada-Carballo, J. M., González-Castaño, F. J., Isasi de Vicente, F., Fernández-Iglesias, M. J.: Jamming System for Mobile Communications, IEE Electronic Letters, 34(22) (1998) 2166–2167.

    Article  Google Scholar 

  35. Pfleeger, S. L., Hatton, L.: Investigating the influence of formal methods, IEEE Computer, 3(2) (1997) 33–43.

    Google Scholar 

  36. Quemada, J., Pavón, S., Fernández, A.: Transforming LOTOS specification with LOLA, in: Turner, K. J., (Ed), Procs. of FORTE’88, North Holland, 1988.

    Google Scholar 

  37. Redl, S. M., Weber, M. K., Oliphant, M. W.: An introduction to GSM, Artech House, 1995.

    Google Scholar 

  38. Steinert, T., Roessler, G.: Generation of Realistic Signalling Traffic in an ISDN Load Test System using SDL User Models, in: Bolognesi, T., Latella, D. Formal Methods for Distributed System Development, Kluwer Academic Publishers, 2000, 219–236.

    Google Scholar 

  39. Voas, J.: Software quality’s eight greatest myths, IEEE Software, 16(5) (1999) 118–120.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Grupo de Ingeniería de Sistemas Telemáticos. Departamento de Tecnologías de las Comunicaciones, Universidade de Vigo, Spain

    Manuel J. Fernández Iglesias, Francisco J. González-Castaño, José M. Pousada Carballo, Martín Llamas Nistal & Alberto Romero Feijoo

Authors
  1. Manuel J. Fernández Iglesias
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Francisco J. González-Castaño
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. José M. Pousada Carballo
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Martín Llamas Nistal
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Alberto Romero Feijoo
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Science Department, University of Minho, Campus de Gualtar, 4700-320, Braga, Portugal

    José Nuno Oliveira

  2. AT&T Laboratories — Research, 180 Park Avenue, Florham Park, New Jersey, 07932, USA

    Pamela Zave

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Iglesias, M.J.F., González-Castaño, F.J., Carballo, J.M.P., Nistal, M.L., Feijoo, A.R. (2001). From Complex Specifications to a Working Prototype. A Protocol Engineering Case Study. In: Oliveira, J.N., Zave, P. (eds) FME 2001: Formal Methods for Increasing Software Productivity. FME 2001. Lecture Notes in Computer Science, vol 2021. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45251-6_25

Download citation

  • DOI: https://doi.org/10.1007/3-540-45251-6_25

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41791-0

  • Online ISBN: 978-3-540-45251-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation