Skip to main content

Formal Specification of Telephone Features

  • Conference paper
Z User Workshop, Cambridge 1994

Part of the book series: Workshops in Computing ((WORKSHOPS COMP.))

Abstract

A full formal specification of the external behavior of a realistic feature set for ISDN telephones is described. In addition to Plain Old Telephone Service, about ten of the most frequently used features of the 5ESSĀ® switch are specified. The connections model deals with shared and multiple directory numbers and billing.

The specification employs a multiparadigm technique in which partial specifications in different languages are composed; this framework is briefly described. This paper focuses on the use of the Z notation to specify call processing and subscriber database aspects of telephone features and the way in which this description is composed with the telephone interface and digit analysis specification. The suitability of the approach for switching software development is discussed.

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

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A. Kay and J. N. Reed. A rely and guarantee method for Timed CSP: A specification and design of a telephone exchange. IEEE Transactions on Software Engineering, Vol. 19, No. 6, June 1993, pp. 625ā€“639.

    Google ScholarĀ 

  2. J. C. P. Woodcock and M. Loomes. Software Engineering Mathematics: Formal Methods Demystified. Pitman, 1988.

    Google ScholarĀ 

  3. Carroll Morgan. Telephone network. In Specification Case Studies (ed. Ian Hayes ), pp. 31ā€“42. Prentice-Hall, second edition 1992.

    Google ScholarĀ 

  4. M. J. Butler. Service extension at the specification level. In Z User Workshop, Oxford 1990 (ed. J. E. Nicholls ), pp. 319ā€“336. Springer-Verlag, 1991.

    Google ScholarĀ 

  5. Pamela Zave and Michael Jackson. Techniques for partial specification and specification of switching systems. In VDM ā€˜81: Formal Software Devel-opment Methods (Proceedings of the Fourth International Symposium of VDM Europe), pp. 511ā€“525. Springer-Verlag, 1991.

    Google ScholarĀ 

  6. V. Petkovic. NSPP Features Users Guide. ATandT Bell Laboratories, Department 55387, 1992.

    Google ScholarĀ 

  7. Pamela Zave and Peter Mataga. A formal specification of some important 5ESSĀ® features, Part I: Overview. ATandT Bell Laboratories Technical Memorandum BL011261ā€“1001ā€“33TM, October 1993.

    Google ScholarĀ 

  8. Pamela Zave and Peter Mataga. A formal specification of some important 5ESSĀ® features, Part II: Telephone states and digit analysis. ATandT Bell Laboratories Technical Memorandum BL011261ā€“1001ā€“34TM, October 1993.

    Google ScholarĀ 

  9. Peter Mataga and Pamela Zave. A formal specification of some important 5ESSĀ® features, Part III: Connections and provisioning. ATandT Bell Laboratories Technical Memorandum BL011265ā€“1001ā€“24TM, October 1993.

    Google ScholarĀ 

  10. Pamela Zave and Michael Jackson. Conjunction as composition. ACM Transactions on Software Engineering and Methodology, Vol. 2, No. 4, October 1993, pp. 379ā€“411.

    ArticleĀ  Google ScholarĀ 

  11. Pamela Zave and Michael Jackson. A multiparadigm specification technique. Draft available from the authors.

    Google ScholarĀ 

  12. Michael Jackson and Pamela Zave. Domain descriptions. In Proceedings of the IEEE International Symposium on Requirements Engineering,pp. 56ā€“64. IEEE Computer Society Press, 1993.

    Google ScholarĀ 

  13. David Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming VIII: 231ā€“274, 1987.

    Google ScholarĀ 

  14. M. A. Jackson. Principles of Program Design. Academic Press, 1975.

    Google ScholarĀ 

  15. J. M. Spivey. The Z Notation: A Reference Manual. Prentice-Hall, second edition 1992.

    Google ScholarĀ 

  16. Alex Borgida, John Mylopoulos and Raymond Reiter. ā€œā€¦And nothing else changesā€: The frame problem in procedure specifications. In Proceedings of the Fifteenth International Conference on Software Engineering,pp. 303ā€“314. IEEE Computer Society Press, 1993.

    Google ScholarĀ 

  17. J. B. Wordsworth. Software Development with Z: A Practical Approach to Formal Methods in Software Engineering. Addison-Wesley, 1992.

    Google ScholarĀ 

  18. J. M. Spivey. The fuzz Manual. Computing Science Consultancy, second edition 1992.

    Google ScholarĀ 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

Ā© 1994 British Computer Society

About this paper

Cite this paper

Mataga, P., Zave, P. (1994). Formal Specification of Telephone Features. In: Bowen, J.P., Hall, J.A. (eds) Z User Workshop, Cambridge 1994. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3452-7_3

Download citation

  • DOI: https://doi.org/10.1007/978-1-4471-3452-7_3

  • Publisher Name: Springer, London

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

  • Online ISBN: 978-1-4471-3452-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics