A meta-method for formal method integration

  • Richard F. PaigeEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1313)


We describe a meta-method for formal method integration [Pai97]. The approach is applied to combining formal methods with other formal and semiformal methods. We discuss the theory behind formal method integration, present two example combinations, and use an integrated method in solving a small problem.


Method Integration Formal Method Invasive Method Method Step Formal Semantic 
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. [Bac90]
    R.J.R. Back. Refinement calculus II: parallel and reactive programs. In Stepwise Refinement of Distributed Systems, LNCS 430, Springer-Verlag, 1990.Google Scholar
  2. [BaV89]
    R.J.R. Back and J. von Wright. A Lattice-Theoretical Basis for a Specification Language. In Mathematics of Program Construction, LNCS 375, Springer-Verlag, 1989.Google Scholar
  3. [BoH94]
    J. Bowen and M. Hinchey. Ten Commandments of Formal Methods. Oxford University Computing Laboratory Technical Monograph, 1994.Google Scholar
  4. [CoY90]
    P. Coad and E. Yourdon. Object-oriented Analysis, Prentice-Hall, 1990.Google Scholar
  5. [DeM79]
    T. DeMarco. Structured Analysis and System Specification, Yourdon Press, 1979.Google Scholar
  6. [DeM82]
    T. DeMarco. Controlling Software Projects: Management, Measurement, and Estimation. Yourdon Press, 1982.Google Scholar
  7. [GuH93]
    J.V. Guttag and J.J. Horning. Larch: Languages and Tools for Formal Specification,. Springer-Verlag, 1993.Google Scholar
  8. [Ha196]
    A. Hall. Using Formal Methods to Develop an ATC Information System. IEEE Software, March 1996.Google Scholar
  9. [Ham94]
    J. Hammond. Producing Z Specifications from Object-Oriented Analysis. In Proc. Eighth Z User Meeting, Cambridge, Springer-Verlag, 1994.Google Scholar
  10. [HeM88]
    E.C.R. Helmer and A.J. Malton. Termination Conventions and Comparative Semantics, Acta Informatica, 25 (1988.Google Scholar
  11. [Heh93]
    E.C.R. Helmer. A Practical Theory of Programming, Springer-Verlag, 1993.Google Scholar
  12. [Hil91]
    J.V. Hill. Software development methods in practice. In Proc. Sixth Annual Conference on Computer Assurance, 1991.Google Scholar
  13. [Hoa85]
    C.A.R. Hoare. Communicating Sequential Processes, Prentice-Hall, 1985.Google Scholar
  14. [Jac95]
    M.A. Jackson. Software Requirements and Specifications, Addison-Wesley, 1995.Google Scholar
  15. [Kin90]
    S. King. Z and the refinement calculus. In VDM `90: VDM and Z-Formal Methods in Software Development, Third international symposium of VDM Europe, LNCS 428, Springer-Verlag, 1990.Google Scholar
  16. [Kro93]
    K. Kronlöf, ed. Method Integration: Concepts and Case Studies, Wiley, 1993.Google Scholar
  17. [LKP91]
    P. Larsen, J. van Katwijk, N. Plat, K. Pronk, and H. Toetenel. Towards an integrated combination of SA and VDM. In Proc. Methods Integration Workshop, Springer-Verlag, 1991.Google Scholar
  18. [MaM88]
    D.A. Marca and C.L. McGowan. SADT-Structured Analysis and Design Technique, McGraw-Hill, 1988.Google Scholar
  19. [Met94]
    Project MetaPHOR Group, MetaPHOR: Metamodeling, Principles, Hypertext, Objects and Repositories. Technical Report TR-7, University of Jyvaskyla, 1994.Google Scholar
  20. [Mor94]
    C.C. Morgan. Programming from Specifications, Prentice-Hall, Second Edition, 1994.Google Scholar
  21. [Pai97]
    R.F. Paige. Formal Method Integration via Heterogeneous Notations, PhD Dissertation, July 1997.Google Scholar
  22. [PWM93]
    F. Polack, M. Whiston, and K.C. Mander. The SAZ Project: Integrating SSADM and Z. In Proc. FME `93: Industrial-strength Formal Methods, LNCS 670, Springer-Verlag, 1993.Google Scholar
  23. [ScR77]
    K. Schoman and D. Ross. Structured Analysis for requirements definition, IEEE Trans. on Software Engineering, 3(1), 1977.Google Scholar
  24. [SFD92]
    L.T. Semmens, R.B. France, and T.W. Docker. Integrated Structured Analysis and Formal Specification Techniques, The Computer Journal 35(6), June 1992.Google Scholar
  25. [Spi89]
    J.M. Spivey. The Z Notation: A Reference Manual, Prentice-Hall, 1989.Google Scholar
  26. [War93]
    N. Ward. Adding specification constructors to the refinement calculus. In Proc. FME `93: Industrial-strength Formal Methods, LNCS 670, Springer-Verlag, 1993.Google Scholar
  27. [WiZ92]
    J.M. Wing and A.M. Zaremski. Unintrusive ways to integrate formal specifications in practice. In VDM `91: Formal Software Development Methods, Fourth International Symposium of VDM Europe, LNCS 551, Springer-Verlag, 1992.Google Scholar
  28. [WoM91]
    J.C.P. Woodcock and C.C. Morgan. Refinement of state-based concurrent systems. In VDM `90: VDM and Z-Formal Methods in Software Development, Third International Symposium of VDM Europe, LNCS 428, Springer-Verlag, 1990.Google Scholar
  29. [YoC79]
    E. Yourdon and L. Constantine. Structured Design, Prentice-Hall, 1979.Google Scholar
  30. [ZaJ93]
    P. Zave and M. Jackson. Conjunction as Composition, ACM Trans. on Software Engineering and Methodology, 2(4), October 1993.Google Scholar
  31. [ZaJ95]
    P. Zave and M. Jackson. Where do operations come from? An approach to multiparadigm specification, IEEE Trans. on Software Engineering, 12(7), July 1996.Google Scholar
  32. [ZaM93]
    P. Zave and P. Mataga. A formal specification of some important 5ESS features, Part 1: Overview. AT&T Bell Laboratories Technical Memorandum, October 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  1. 1.Department of Computer ScienceUniversity of TorontoTorontoCanada

Personalised recommendations