Skip to main content
SpringerLink
Log in

Integrating Formal Methods into a Professional Master of Software Engineering Program

  • Conference paper
Z User Workshop, Cambridge 1994

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

Abstract

A critical issue in the design of a professional software engineering degree program is the way in which formal methods are integrated into the curriculum. The approach taken by most programs is to teach formal techniques for software development in a separate course on formal methods. In this paper we detail some of the problems with that approach and describe an alternative in which formal methods are integrated across the curriculum. We illustrate the strengths and weaknesses of this alternative in terms of our experience of using it in the Master of Software Engineering Program at Carnegie Mellon University.

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 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. Gregory Abowd, Robert Allen, and David Garlan. Using style to give meaning to software architecture. In Procedings of SIGSOFT’93: Foundations of Software Engineering, December 1993.

    Google Scholar 

  2. Robert Allen and David Garlan. A formal approach to software architectures. In Jan van Leeuwen, editor, Proceedings of IFIP’92. Elsevier Science Publishers B.V., September 1992. An expanded version appears as CMU School of Computer Science Technical Report CMU-CS-92–163, Towards Formalized Software Architectures.

    Google Scholar 

  3. Robert Allen and David Garlan. Formalizing architectural connection. In Proceedings of the Sixteenth International Conference on Software Engineering, May 1994.

    Google Scholar 

  4. G. Barrett. Formal methods applied to a floating-point number system. IEEE Transactions on Software Engineering, 15 (5): 611–621, May 1989.

    Article  Google Scholar 

  5. W.C. Bowman, G.H. Archinoff, V.M. Raina, D.R. Tremaine, and N.G. Leveson. An application of fault tree analysis to safety critical software at Ontario Hydro. In Conference on Probabilistic Safety Assessment and Management (PSAM), April 1991.

    Google Scholar 

  6. Norman Delisle and David Garlan. Applying formal specification to industrial problems: A specification of an oscilloscope. IEEE Software, 7 (5): 29–37, September 1990.

    Article  Google Scholar 

  7. Gary Ford. 1991 sei report on graduate software engineering education. Technical Report CMU/SEI-911-TR-2, CMU Software Engineering Institute, April 1991.

    Google Scholar 

  8. David Garlan. Preconditions for understanding. In Proceedings of the Fourth International Workshop on Software Specification and Design, pages 242–245. IEEE Society Press, October 1991.

    Google Scholar 

  9. David Garlan. Formal methods for software engineers: Tradeoffs in curriculum design. In Proceedings of the Sixth SEI Conference on Software Engineering Education. Springer Verlag, October 1992.

    Google Scholar 

  10. David Garlan. Formal approaches to software architecture. In David Alex Lamb and Sandra Crocker, editors, Proceedings of the Workshop on Studies of Software Design, number ISSN–0836–022793–352 in External Technical Report, Baltimore, Maryland, May 1993. Queen’s University Department of Computing and Information Science.

    Google Scholar 

  11. David Garlan, Alan Brown, Daniel Jackson, Jim Tomayko, and Jeannette Wing. The CMU Masters in Software Engineering core curriculum. Technical Report CMU-CS-93–180, Carnegie Mellon University, August 1993.

    Google Scholar 

  12. J.V. Guttag and J.J. Horning. Formal specification as a design tool. In Seventh POPL. ACM, 1980. (also in Software Specification Techniques,pages 187–207).

    Google Scholar 

  13. David Garlan and David Notkin. Formalizing design spaces: Implicit invocation mechanisms. In VDM’91: Formal Software Development Methods, pages 31–44. Springer-Verlag, LNCS 551, October 1991.

    Google Scholar 

  14. D. Gries. The Science of Programming. Springer-Verlag, 1981.

    Google Scholar 

  15. David Garlan, Mary Shaw, Chris Okasaki, Curtis Scott, and Roy Swonger. Experience with a course on architectures for software systems. In Proceedings of the Sixth SEI Conference on Software Engineering Education. Springer Verlag, LNCS 376, October 1992. Also available as a CMU/SEI technical report, CMU/SEI-92-TR17.

    Google Scholar 

  16. D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8: 231–274, 1987.

    Article  MathSciNet  MATH  Google Scholar 

  17. C.A.R. Hoare. Proof of correctness of data representations. Acta Informatica, 1: 271–281, 1972.

    Article  MATH  Google Scholar 

  18. C.A.R. Hoare. Communicating sequential processes. CA CM, 21 (8): 666–677, August 1978.

    Google Scholar 

  19. C.B. Jones. Systematic program development. In Proc. Symposium on Mathematics and Computer Science,1986. (also in Software Specification Techniques,pages 89–108).

    Google Scholar 

  20. K. L. McMillan. The SMV system, February 1992. Draft.

    Google Scholar 

  21. K. McMillan and J. Schwalbe. Formal verification of the Encore Gigamax cache consistencey protocol. In International Symposium on Shared Memory Multiprocessors, 1991.

    Google Scholar 

  22. C.J. Nix and B.P. Collins. The use of software engineering, including the Z notation, in the development of CICS. Quality Assurance, 14 (3): 103–110, September 1988.

    Google Scholar 

  23. H. Penny Nii. Blackboard systems Part 1: The blackboard model of problem solving and the evolution of blackboard architectures. AI Magazine,7(3):38–53, Summer 1986. Reprinted with corrections by AI Magazine.

    Google Scholar 

  24. H. Penny Nii. Blackboard systems Part 2: Blackboard application systems and a knowledge engineering perspective. AI Magazine,7(4):82–107, August 1986. Reprinted with corrections by AI Magazine.

    Google Scholar 

  25. Neil R. Reizer, Gregory D. Abowd, B. Craig Meyers, and Patrick R.H. Place. Using formal methods for requirements specification of a proposed POSIX standard. In Proceedings of the International Conference on Requirements Engineering, 1994.

    Google Scholar 

  26. Lui Sha and John B. Goodenough. Real-time scheduling theory and Ada*. Computer, pages 53–62, April 1990.

    Google Scholar 

  27. Mary Shaw. Prospects for an engineering discipline of software. IEEE Software, 7 (6): 15–24, November 1990.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Carnegie Mellon University, 5000 Forbes Avenue, Pittsburgh, PA, 15213, USA

    David Garlan

Authors
  1. David Garlan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Programming Research Group, Oxford University Computing Laboratory, Wolfson Buliding, Parks Road, OX1 3QD, Oxford, UK

    J. P. Bowen MA

  2. Praxis Systems plc, 20 Manvers Street, BA1 1PX, Bath, UK

    J. A. Hall MA, DPhil, CEng

Rights and permissions

Reprints and permissions

Copyright information

© 1994 British Computer Society

About this paper

Cite this paper

Garlan, D. (1994). Integrating Formal Methods into a Professional Master of Software Engineering Program. 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_5

Download citation

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

  • 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

Search

Navigation