Advertisement

Formal Methods and Industrial-Strength Computer Networks

  • Joy Reed
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1526)

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.

Keywords

Formal Methods Network Protocols CSP FDR 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. BC95.
    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. But92.
    Butler, R.: A CSP Approach to Action Systems, DPhil Thesis, University of Oxford (1992)Google Scholar
  3. BZB96.
    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. cgj95.
    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. Cre.
    Creese, S.: An inductive technique for modelling arbitrarily configured networks, MSc Thesis, University of Oxford (1997)Google Scholar
  6. CR.
    Creese, S., Reed, J.: Inductive Properties and Automatic Proof for Computer Networks (to appear)Google Scholar
  7. Dav91.
    Davies, J.: Specification and Proof in Real-time Systems, D.Phil Thesis, Univ. of Oxford (1991)Google Scholar
  8. FDR.
    Formal Systems (Europe) Ltd: Failures Divergence Refinement. User Manual and Tutorial, version 1.4 (1994)Google Scholar
  9. ftpe.
  10. GJ94.
    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. GPB91.
    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. Hoa85.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)zbMATHGoogle Scholar
  13. ISOE.
    ISO Recommendation 9074, The Extended State Transition Language, Estelle (1989)Google Scholar
  14. ISOL.
    ISO: Information Processing System - Open System Interconnection - LOTOS -A Formal Description Technique based on Temporal Ordering of Observational Behavior, IS8807 (1988)Google Scholar
  15. Jac96.
    Jackson, D.M.: Experiences in Embedded Scheduling. In: Formal Methods Europe, Oxford (1996)Google Scholar
  16. Jma95.
    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. KR93.
    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)CrossRefGoogle Scholar
  18. km89.
    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. LY93.
    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. NM90.
    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. PS91.
    Paliwoda, K., Sanders, J.W.: An Incremental Specification of the Sliding-window Protocol. Distributed Computing, 83–94 (May 1991)Google Scholar
  22. R98.
    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. RGG95.
    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, HeidelbergGoogle Scholar
  24. Ros97.
    Roscoe, A.W.: The CSP Handbook. Prentice-Hall International, Englewood Cliffs (1997)Google Scholar
  25. RR86.
    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-261Google Scholar
  26. S98.
    Scattergood, B.: Tools for CSP and Timed CSP, University of Oxford, DPhil Thesis (forthcoming, 1998)Google Scholar
  27. Shan.
    Shankar, N.: Machine-Assisted Verification Using Automated Theorem Proving and Model Checking. In: Broy, M. (ed.) Math. Prog. MethodologyGoogle Scholar
  28. Sid93.
    Sidle, K.: Pi Bus. Formal Methods Europe, Barcelona (1993)Google Scholar
  29. Sin97.
    Sinclair, J.: Action Systems, Determinism, and the Development of Secure Systems, PHd Thesis, Open University (1997)Google Scholar
  30. Tan96.
    Tanenbaum, A.S.: Computer Networks, 3rd edn. Prentice-Hall, Englewood Cliffs (1996)Google Scholar
  31. TCSP92.
    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. Tur86.
    Turner, J.S.: New Directions in Communications (or Which Way to the Information Age). IEEE Commun. Magazine 24, 8–15 (1986)CrossRefGoogle Scholar
  33. wl89.
    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. wwwl.
  35. ZDE93.
    Zhang, L., Deering, S., Estrin, D., Shenker, S., Zappala, D.: RSVP: A New Resource Reservation Protocol. IEEE Network (September 1993)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Joy Reed
    • 1
  1. 1.Oxford Brookes UniversityOxfordUK

Personalised recommendations