Formal methods for software engineers: Tradeoffs in curriculum design

  • David Garlan
Session 4: Formal Methods and Engineering Instruction
Part of the Lecture Notes in Computer Science book series (LNCS, volume 640)


While formal methods are becoming increasingly important to software engineering, currently there is little consensus on how they should be taught. In this paper I outline some of the important dimensions of curriculum design for formal methods and illustrate the tradeoffs through a brief examination of four common course formats. I summarize what I have learned from teaching courses in each of these formats and outline an agenda of educational research that will enable us to teach formal methods more effectively.


Software Engineering Software Engineer Formal Method Curriculum Design Formal Notation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Age79]
    T. Agerwala. Putting Petri nets to work. Computer, 12(12):85–94, December 1979.Google Scholar
  2. [AK84]
    B. Auernheimer and R.A. Kemmerer. ASLAN User's Manual. Dept. of Computer Science, UC Santa Barbara, 1984.Google Scholar
  3. [Bar89]
    G. Barrett. Formal methods applied to a floating-point number system. IEEE Transactions on Software Engineering, 15(5):611–621, May 1989.Google Scholar
  4. [BAR+91]
    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
  5. [BCM+90]
    J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, June 1990.Google Scholar
  6. [Cal86]
    Problem set for the fourth international workshop on software specification and design. ACM SIGSOFT Engineering Notes, April 1986, 1986.Google Scholar
  7. [CHJ86]
    B. Cohen, W.T. Harwood, and M.I. Jackson. The Specification of Complex Systems. Addison-Wesley, 1986. (Chapter 5: Model-based specification).Google Scholar
  8. [CM78]
    J.P. Cavano and J.A. McCall. A framework for the measurement of software quality. In Software Quality and Assurance Workshop, pages 133–139. ACM, November 1978.Google Scholar
  9. [DG90]
    N. Delisle and D. Garlan. A formal specification of an oscilloscope. Software, 7(5):29–37, September 1990.Google Scholar
  10. [GD90]
    David Garlan and Norman Delisle. Formal specifications as reusable frameworks. In VDM'90: VDM and Z — Formal Methods in Software Development, Kiel, Germany, 1990. Springer-Verlag, LNCS 428.Google Scholar
  11. [GH80]
    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
  12. [GHM78]
    J.V. Guttag, E. Horowitz, and D.R. Musser. Abstract data types and software validation. Communications of the ACM, 21(12), December 1978.Google Scholar
  13. [GHM90]
    J.V. Guttag, J.J. Horning, and M. Modet. Report on the Larch Shared Language: Version 2.3. Technical Report 58, Digital, Systems Research Center, 1990.Google Scholar
  14. [GHW85]
    J.V. Guttag, J.J. Horning, and J.M. Wing. The Larch family of specification languages. IEEE Software, 2(5):24–36, September 1985.Google Scholar
  15. [GN91]
    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
  16. [Gri81]
    D. Gries. The Science of Programming. Springer-Verlag, 1981.Google Scholar
  17. [Hal90]
    A. Hall. Seven myths of formal methods. Software, 7(5):11–20, September 1990.Google Scholar
  18. [Hoa72]
    C.A.R. Hoare. Proof of correctness of data representations. Acta Informatica, 1:271–281, 1972.Google Scholar
  19. [Hoa78]
    C.A.R. Hoare. Communicating sequential processes. CACM, 21(8):666–677, August 1978.Google Scholar
  20. [ISO87]
    ISO. Information processing systems — open systems interconnection — LOTOS — a formal description technique based on the temporal ordering of observational behaviour. Technical Report ISO/TC 97/SC 21, International Standards Organization, 1987.Google Scholar
  21. [Jon86]
    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
  22. [Kem85]
    R.A. Kemmerer. Testing formal specifications to detect design errors. IEEE Transactions on Software Engineering, 11(1):32–43, January 1985.Google Scholar
  23. [MoD89]
    Requirements for the procurement of safety critical software in defense equipment. U.K. Ministry of Defense, May 1989. Interim Defence Standard 00-55.Google Scholar
  24. [MS84]
    C. Carroll Morgan and Bernard A. Sufrin. Specification of the Unix filing system. IEEE Transactions on Software Engineering, 10(2):128–142, March 1984.Google Scholar
  25. [MS91]
    K. McMillan and J. Schwalbe. Formal verification of the Encore Gigamax cache consistencey protocol. In International Symposium on Shared Memory Multiprocessors, 1991.Google Scholar
  26. [NC88]
    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
  27. [OL82]
    S. Owicki and L. Lamport. Proving liveness properties of concurrent programs. ACM Transactions on Programming Languages and Systems, 4(3):455–495, July 1982.Google Scholar
  28. [PC86]
    D.L. Parnas and P.C. Clements. A rational design process: How and why to fake it. IEEE Transactions on Software Engineering, SE-12(2):251–257, February 1986.Google Scholar
  29. [Pet77]
    J.L. Peterson. Petri nets. ACM Computing Surveys, 9(3):223–252, September 1977.Google Scholar
  30. [Pou89]
    D. Pountain. Occam II. Byte, 14(10):279–284, October 1989.Google Scholar
  31. [SG90]
    Lui Sha and John B. Goodenough. Real-time scheduling theory and Ada.* Computer, pages 53–62, April 1990.Google Scholar
  32. [SIG91]
    Proceedings of the ACM SIGSOFT'91 Conference on Software for Critical Systems, Software Engineering Notes, Volume 16, Number 5. ACM Press, December 1991.Google Scholar
  33. [Spi88]
    J.M. Spivey. The Fuzz manual, 1988.Google Scholar
  34. [Spi89]
    J.M. Spivey. An introduction to Z and formal specification. Software Engineering Journal, 4(1):40–50, January 1989.Google Scholar
  35. [ST91]
    Mary Shaw and James E. Tomayko. Models for undergraduate project courses in software engineering. In Proceedings Fifth SEI Conference on Software Engineering Education, October 1991.Google Scholar
  36. [Ste88]
    R.M. Stein. T800 and counting. Byte, 13(12):287–296, November 1988.Google Scholar
  37. [Win90]
    J. Wing. A specifier's introduction to formal methods. Computer, 23(9):8–26, September 1990.Google Scholar
  38. [Zar91]
    A.M. Zaremski. A Larch specification of the Miro Editor. Technical Report CMU-CS-91-111, Carnegie Mellon University, 1991.Google Scholar
  39. [Zav82]
    P. Zave. An operational approach to requirements specification for embedded systems. IEEE Trans. on Software Engineering, SE-8(3), 1982. (also in Software Specification Techniques, pages 131–169).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • David Garlan
    • 1
  1. 1.School of Computer ScienceCarnegie Mellon UniversityPittsburgh

Personalised recommendations