Skip to main content
SpringerLink
Log in

Formal Methods and Industrial-Strength Computer Networks

  • Conference paper
Book cover Requirements Targeting Software and Systems Engineering (RTSE 1997)

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

  • 263 Accesses

Abstract

Two case studies involving the application of formal methods to industrial-strength computer networks are described. In both case studies, the formal method (CSP/FDR) was thought sufficiently mature for these applications. However in both cases, for the formal method to be effective it was necessary to develop techniques requiring expert knowledge in the theory underpinning the formal method. These examples illustrate that there remain significant technical challenges to effective use of formal methods, which come to light only through large-scale applications.

This work was supported in part by the US Office of Naval Research.

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

Access this chapter

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 74.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Barnard, D., Crosby, S.: The Specification and Verification of an Experimental ATM Signalling Protocol. In: Dembrinski, Sredniawa (eds.) Proc. IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification, Warsaw, Poland, vol. XV. Chapman Hall, Boca Raton (1995)

    Google Scholar 

  2. Butler, R.: A CSP Approach to Action Systems, DPhil Thesis, University of Oxford (1992)

    Google Scholar 

  3. Braden, R., Zhang, L., Berson, S., Herzog, S., Jamin, S.: Resource reSerVation Protocol (RSVP) – Version 1, Functional Specification. In: Internet Draft, Internet Engineering Task Force (1996)

    Google Scholar 

  4. Clarke, E.M., Grumberg, O., Jha, S.: Verifying parameterized networks using abstraction and regular languages. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962. Springer, Heidelberg (1995)

    Google Scholar 

  5. Creese, S.: An inductive technique for modelling arbitrarily configured networks, MSc Thesis, University of Oxford (1997)

    Google Scholar 

  6. Creese, S., Reed, J.: Inductive Properties and Automatic Proof for Computer Networks (to appear)

    Google Scholar 

  7. Davies, J.: Specification and Proof in Real-time Systems, D.Phil Thesis, Univ. of Oxford (1991)

    Google Scholar 

  8. Formal Systems (Europe) Ltd: Failures Divergence Refinement. User Manual and Tutorial, version 1.4 (1994)

    Google Scholar 

  9. Estelle Specifications, ftp://louie.udel.edu/pub/grope/estelle-specs

  10. Guttman, J.D., Johnson, D.M.: Three Applications of Formal Methods at MITRE. In: Naftolin, M., Denfir, T. (eds.) FME 1994. LNCS, vol. 873. Springer, Heidelberg (1994)

    Google Scholar 

  11. Groz, R., Phalippou, M., Brossard, M.: Specification of the ISDN Linc Access Protocol for D-channel (LAPD), CCITT Recommendation Q.921, ftp://louie.udel.edu/pub/grope/estelle-specs/lapd.e

  12. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)

    MATH  Google Scholar 

  13. ISO Recommendation 9074, The Extended State Transition Language, Estelle (1989)

    Google Scholar 

  14. ISO: Information Processing System - Open System Interconnection - LOTOS -A Formal Description Technique based on Temporal Ordering of Observational Behavior, IS8807 (1988)

    Google Scholar 

  15. Jackson, D.M.: Experiences in Embedded Scheduling. In: Formal Methods Europe, Oxford (1996)

    Google Scholar 

  16. Jmail, M., Dembrinski, Sredniawa: An Algebraic-temporal Specification of a CSMA/CD Protocol. In: Proc. IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification, Warsaw, Poland, 1995, vol. XV. Chapman Hall, Boca Raton (1995)

    Google Scholar 

  17. Kay, A., Reed, J.N.: A Rely and Guarantee Method for TCSP, A Specification and Design of a Telephone Exchange. IEEE Trans. Soft. Eng. 19, 625–629 (1993)

    Article  Google Scholar 

  18. Kurshan, R.P., McMillan, M.: A structural induction theorem for processes. In: Proceedings of the Eighth ACM Symposium on Principles of Distributed Computing (1989)

    Google Scholar 

  19. Leon, G., Yelmo, J.C., Sanchez, C., Carrasco, F.J., Gil, J.J.: An Industrial Experience on LOTOS-based Prototyping for Switching Systems Design. In: Woodcock, J.C.P., Larsen, D.G. (eds.) FME 1993. LNCS, vol. 670. Springer, Heidelberg (1993)

    Google Scholar 

  20. Navarro, J., Martin, P.S.: Experience in the Development of an ISDN Layer 3 Service in LOTOS. In: Quemada, J., Manas, J.A., Vazquez, E. (eds.) Proc. Formal Description Techniques III. North-Holland, Amsterdam (1990)

    Google Scholar 

  21. Paliwoda, K., Sanders, J.W.: An Incremental Specification of the Sliding-window Protocol. Distributed Computing, 83–94 (May 1991)

    Google Scholar 

  22. Reed, J.N., Jackson, D.M., Deianov, B., Reed, G.M.: Automated Formal Analysis of Networks: FDR Models of Arbitrary Topologies and Flow-Control Mechanisms. In: ETAPS-FASE 1998 European Joint Conference on Theory and Practice of Software (1998); Fundamental Approaches to Software Engineering, Lisbon Portugal (March 1998)

    Google Scholar 

  23. Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M.H., Hulance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical compression for model-checking CSP or How to check 1020 dining philosophers for deadlock. LNCS, vol. 1019. Springer, Heidelberg

    Google Scholar 

  24. Roscoe, A.W.: The CSP Handbook. Prentice-Hall International, Englewood Cliffs (1997)

    Google Scholar 

  25. Reed, G.M., Roscoe, A.W.: A timed model for communicating sequential processes. In: Kott, L. (ed.) ICALP 1986. LNCS, vol. 226, pp. 314–323. Springer, Heidelberg (1986); Theoretical Computer Science 58, 249-261

    Google Scholar 

  26. Scattergood, B.: Tools for CSP and Timed CSP, University of Oxford, DPhil Thesis (forthcoming, 1998)

    Google Scholar 

  27. Shankar, N.: Machine-Assisted Verification Using Automated Theorem Proving and Model Checking. In: Broy, M. (ed.) Math. Prog. Methodology

    Google Scholar 

  28. Sidle, K.: Pi Bus. Formal Methods Europe, Barcelona (1993)

    Google Scholar 

  29. Sinclair, J.: Action Systems, Determinism, and the Development of Secure Systems, PHd Thesis, Open University (1997)

    Google Scholar 

  30. Tanenbaum, A.S.: Computer Networks, 3rd edn. Prentice-Hall, Englewood Cliffs (1996)

    Google Scholar 

  31. Davies, J., Jackson, D.M., Reed, G.M., Reed, J.N., Roscoe, A.W., Schneider, S.A.: Timed CSP: Theory and practice. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600. Springer, Heidelberg (1992)

    Google Scholar 

  32. Turner, J.S.: New Directions in Communications (or Which Way to the Information Age). IEEE Commun. Magazine 24, 8–15 (1986)

    Article  Google Scholar 

  33. Wolper, P., Lovinfosse, V.: Verifying Properties of Large Sets of Processes with Network Invariants. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407. Springer, Heidelberg (1990)

    Google Scholar 

  34. LOTOS Bibliography, http://www.cs.stir.ac.uk/kjt/research/well/bib.html

  35. Zhang, L., Deering, S., Estrin, D., Shenker, S., Zappala, D.: RSVP: A New Resource Reservation Protocol. IEEE Network (September 1993)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Oxford Brookes University, Oxford, UK

    Joy Reed

Authors
  1. Joy Reed
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Technische Universität München, Germany

    Manfred Broy

  2. Institute for Software Systems Engineering, Braunschweig University of Technology, Mühlenpfordtstraße 23, 38106, Braunschweig, Germany

    Bernhard Rumpe

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Reed, J. (1998). Formal Methods and Industrial-Strength Computer Networks. In: Broy, M., Rumpe, B. (eds) Requirements Targeting Software and Systems Engineering. RTSE 1997. Lecture Notes in Computer Science, vol 1526. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10692867_10

Download citation

  • DOI: https://doi.org/10.1007/10692867_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65309-7

  • Online ISBN: 978-3-540-49439-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation